proposition: Lemma highPtUn2 A1 A2 h1 h2 (x1 x2 : ptr) (v1 : A1) (v2 : A2) : def (x1 :-> v1 :+ h1) -> def (x2 :-> v2 :+ h2) -> high x1 -> high x2 -> h1 =~ h2 -> x1 :-> v1 :+ h1 =~ x2 :-> v2 :+ h2.
proof: Proof. by move=>D1 D2 H1 H2 L; apply: lowUn=>//; apply: highPn. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep