proposition: Lemma sexit4 h : def h -> (def empty -> empty = empty) -> supdom h h.
proof: Proof. by move=>*; rewrite -(un0h h); apply: subdomE=>//; rewrite un0h. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep