proposition: Lemma defFUn h1 h2 x : def (h1 :+ h2) -> def (free x h1 :+ h2).
proof: Proof. case: defUn=>// H1 H2 H _. case: defUn=>//; [by rewrite defF H1|by rewrite H2|]. move=>k; rewrite domF inE /=. by case: ifP=>_ //; move/H; move/negbTE=>->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep