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