proposition: Lemma empty_alt (x := IM (fun z: False => bool)) : x = emptyset.
proof: Proof. have H t: ~ (inc t x) by move /IM_P => [y]; case: y. set_extens t; [ case/H | case; case ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)