proposition: Lemma noaliasR_fwd3 s (f : Scan.form s) (D : def f) x y (g : check x y s) : x != y_of g.
proof: Proof. case: f D=>h A /= D. case: A g=>// U _ [y' /= ->]. by apply. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)