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