proposition: Lemma unKhl h h1 h2 : def (h1 :+ h) -> h1 :+ h = h2 :+ h -> h1 = h2.
proof: Proof. case: h h1 h2=>[|h H]; case=>[|h1 H1]; case=>[|h2 H2] //=; rewrite /union2; case: ifP=>//; case: ifP=>// D1 D2 _ [E]; apply/heapE. by apply: fcatsK E; rewrite D1 D2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep