proposition: Lemma lowPtUn A1 A2 h1 h2 (x : ptr) (v1 : A1) (v2 : A2) : def (x :-> v1 :+ h1) -> def (x :-> v2 :+ h2) -> (x :-> v1 :+ h1 =~ x :-> v2 :+ h2) = (h1 =~ h2).
proof: Proof. move=>D1 D2. case E: (h1 =~ h2); first by apply: lowUn. move/(elimF idP): E=>E; apply: (introF idP)=>F; case: E. by apply: loweqK F. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep