proposition: Lemma sexit3 h1 h : def h -> (def empty -> supdom empty h1) -> supdom h (h :+ h1).
proof: Proof. move=>H1 H2; rewrite unC -{1}(un0h h). by apply: subdomE; [rewrite un0h | apply: H2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep