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