@[export lean_grind_mk_eq_proof]
Returns a proof that a = b
.
It assumes a
and b
are in the same equivalence class.
Equations
Instances For
@[export lean_grind_mk_heq_proof]
Returns a proof that a = b
.
It assumes a
and b
are in the same equivalence class.