A slow unification call in an unknown version of Lean

slow.lean

class op {T : Type} := (op_op : T -> T -> T)
instance nat_op : @op nat := op.mk (nat.add)

def tc_op {T:Type} [o : @op T] : T -> T -> T := @op.op_op T o
infixl `#`:50 := tc_op

def mk_evar (n : nat) := n

section test
theorem test {a b c d e f g h j i k l m n o p q r s t u v w: nat} : true :=
  begin
    have h: (
    (a # b # c # d # e # f # g # h # i # j # k # _ # l)
              =
                  (_ # a # b # c # d # e # f # g # h # i # j # k # _ # m)),
              refl
  end
end test