proposition: Lemma freeUnr h1 h2 x : x \notin dom h2 -> free x (h1 :+ h2) = free x h1 :+ h2.
proof: Proof. by move=>H; rewrite unC freeUnl // unC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep