rewrite tactic fails when the equation contains several metavariables

[fblanqui]

In Stdlib.List:

opaque symbol rot_size [a] (l:𝕃 a) : π (rot (size l) l = l) ≔
begin
  assume a l; simplify; rewrite take_size l;
flag "print_implicits" on;
rewrite drop_size;
  reflexivity;
end;

fails with

No subterm of [@= (list a) (@++ a (@drop a (@size a l) l) l) l] matches [@drop ?11 (@size ?11 l) l]