proposition: Lemma subdomP h1 h2 : def h1 -> ~~ empb h1 -> reflect {subset dom h1 <= dom h2} (subdom h1 h2).
proof: Proof. case: h1 h2=>[|h1 H1] // [|h2 H2] //= _ H3; last by apply: allP. apply: ReflectF. suff H: head null (supp h1) \in supp h1 by move/(_ _ H). by case: (supp h1) H1 H3=>[|x xs] //=; rewrite !inE eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep