proposition: Lemma subdom_refl h : def h -> subdom h h.
proof: Proof. by case: h=>[//|h H _]; apply/allP. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep