proposition: Lemma highPtUn A h1 h2 (x : ptr) (v : A) : def (x :-> v :+ h1) -> high x -> (x :-> v :+ h1 =~ h2) = (h1 =~ h2).
proof: Proof. move=>D H. case E: (h1 =~ h2); case: loweqP E=>// L1 _; apply/loweqP. - move=>y; rewrite !ldomP domPtUn !inE D. case: eqP=>[<-|]; last by rewrite -!ldomP L1. by rewrite lhE H /= andbF. move=>L2; case: L1 => y; move: {L2} (L2 y). rewrite !ldomP !domPtUn !inE D /=. by case: eqP=>//= <-; rewrite lhE H andbF -[x \in dom h1]negbK (defPt_dom D). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep