@dselsam The method `try_user_congr` was leaking a temporary
meta-variable into the formula. The problem in the congruence lemma
```
dif_ctx_simp_congr :
∀ {α : Sort u_1} {b c : Prop} [dec_b : decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
(h_c : b ↔ c),
(∀ (h : c), x (h_c.mpr h) = u h) →
(∀ (h : ¬c), y ((not_iff_not_of_iff h_c).mpr h) = v h) → dite b x y = dite c u v
```
when the hypothesis `(∀ (h : c), x (h_c.mpr h) = u h)` is processed,
`h_c` is still unassigned. `h_c` was being assigned in a second
loop (the one that I deleted). Do you see any reason for having this
second pass? I think it is an optimization, we can skip the potentially
expensive
```
expr hyp = finalize(m_ctx, rel, r_congr_hyp).get_proof();
expr pf = local_factory.mk_lambda(hyp);
```
if the expression has not been simplified.
Anyway, I removed this code and merged both loops.
I don't think it should impact performance since we barely use custom
congruence lemmas.
68afd4194b