proposition: Lemma unDl2 h1 h2 : def2 (h1 :++ h2) -> def2 h1.
proof: Proof. by case/andP=>/= D1 D2; rewrite /def2 (defUnl D1) (defUnl D2). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep