proposition: Lemma defUnF h1 h2 x : def (h1 :+ h2) -> def (h1 :+ free x h2).
proof: Proof. by rewrite unC; move/(defFUn x); rewrite unC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep