proposition: Lemma noaliasR2 s x y (f : Scan.form s) (g : NoAlias2.form x y s) : def f -> NoAlias2.eq_of g.
proof: Proof. by case: f=> [h] H /H [U _]; case: g=> [] /= ? /(_ U). Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps noalias)