proposition: Lemma highPn A1 A2 (x1 x2 : ptr) (v1 : A1) (v2 : A2) : high x1 -> high x2 -> x1 :-> v1 =~ x2 :-> v2.
proof: Proof. move=>H1 H2. apply/loweqP=>y; rewrite !ldomP !domPt !inE. case E1: (x1 == y); first by rewrite -(eqP E1) lhE H1 !andbF. case E2: (x2 == y)=>//=. by rewrite -(eqP E2) lhE H2 andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep