proposition: Lemma noaliasR h x y (sc : Scan h) (s2 : Search2 x y seq_of): def h -> x != y.
proof: Proof. move=>D. by case: sc s2=>s /= [//|] U _ [/= [_ _ H3]]; apply: H3. Qed.
imports: mathcomp(ssreflect ssrbool seq eqtype) LemmaOverloading(heaps)