proposition: Lemma freeUnD h1 h2 x : def (h1 :+ h2) -> free x (h1 :+ h2) = free x h1 :+ free x h2.
proof: Proof. move=>D; rewrite freeUn domUn D !inE /=; case: ifP=>//. by move/negbT; rewrite negb_or; case/andP=>H1 H2; rewrite !dom_free. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep