proposition: Lemma unC : forall h1 h2, h1 :+ h2 = h2 :+ h1.
proof: Proof. case=>[|h1 H1]; case=>[|h2 H2] //; rewrite /union2. by case: ifP=>E; rewrite disjC E // -heapE fcatC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep