proposition: Lemma subdomQ x h1 h2 : subdom h1 h2 -> x \in dom h1 -> x \in dom h2.
proof: Proof. move=>S H; case: subdomP S=>//. - by apply: dom_def H. - by case: empP=>// E; rewrite E dom0 in H. by move=>H2 _; apply: H2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep