proposition: Lemma noaliasR s x (f : Scan.form s) (g : NoAlias3.form x s) : def f -> x != NoAlias3.y_of g.
proof: Proof. by move: f g=>[[h]] H1 [[y']] /= H2; case/H1=>U _; apply: H2. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps noalias)