proposition: Lemma subheap_id hp1 hp2: subheap hp1 hp2 -> subheap hp2 hp1 -> hp1 = hp2.
proof: Proof. move=>S12; move: (S12) => [D12 _]. move/andP: (subdom_def D12) S12=>{D12} [D1 D2]. case: hp1 D1=>[//=|fm1 pf1]. case: hp2 D2=>[//=|fm2 pf2] _ _ [S12 L12] [S21 L21]. rewrite -heapE; apply: fmapP => k. move: (@subdomQ k _ _ S12) (@subdomQ k _ _ S21) => S'12 S'21. move: (L12 k) (L21 k). case H1: (k \in dom (Def pf1)). - move: (S'12 H1)=> H2. case F1: (fnd k fm1)=> [d1|]; case F2: (fnd k fm2)=> [d2|] //=; rewrite F1 F2. - by move=>H; rewrite (H is_true_true). - by move: (fnd_supp_in H2); rewrite F2=> [[v]]. - by move: (fnd_supp_in H1); rewrite F1=> [[v]]. case H2 : (k \in dom (Def pf2)). - by rewrite (S'21 H2) in H1. move => _ _; rewrite /dom -topredE in H2. by rewrite (fnd_supp (negbT H1)) (fnd_supp (negbT H2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep