proposition: Lemma freeUnl h1 h2 x : x \notin dom h1 -> free x (h1 :+ h2) = h1 :+ free x h2.
proof: Proof. move=>D1; rewrite freeUn domUn !inE (negbTE D1) /=. case: ifP; first by case/andP; rewrite dom_free. move/negbT; rewrite negb_and; case/orP=>D2; last by rewrite dom_free. suff: ~~ def (h1 :+ free x h2). - by case: (h1 :+ free x h2)=>// _; case: (h1 :+ h2) D2. apply: contra D2; case: defUn=>// H1 H2 H _. case: defUn=>//; first by [rewrite H1]; first by move: H2; rewrite defF=>->. move=>k H3; move: (H _ H3); rewrite domF inE /=. by case: ifP H3 D1=>[|_ _ _]; [move/eqP=><- -> | move/negbTE=>->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep