proposition: Lemma freeUn h1 h2 x : free x (h1 :+ h2) = if x \in dom (h1 :+ h2) then free x h1 :+ free x h2 else h1 :+ h2.
proof: Proof. case: h1 h2=>[|h1 H1] [|h2 H2] //; rewrite /union2 /free /dom /=. case: ifP=>E1 //; rewrite supp_fcat inE /=. case: ifP=>E2; last by apply/heapE; rewrite rem_supp // supp_fcat inE /= E2. rewrite disj_rem; last by rewrite disjC disj_rem // disjC. apply/heapE; case/orP: E2=>E2. - suff E3: x \notin supp h2 by rewrite -fcat_rems // (rem_supp E3). by case: disjP E1 E2=>// H _; move/H. suff E3: x \notin supp h1 by rewrite -fcat_srem // (rem_supp E3). by case: disjP E1 E2=>// H _; move/contra: (H x); rewrite negbK. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep