proposition: Lemma sup_defdef h1 h2 : def h2 -> supdom h2 h1 -> def h1.
proof: Proof. by move=>H1; rewrite /supdom; move/subdom_def; rewrite H1 andbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep