proposition: Lemma subdom_def h1 h2 : subdom h1 h2 -> def h1 && def h2.
proof: Proof. by case: h1 h2=>[|h1 H1] // [|h2 H2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep