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