proposition: Lemma not_in_subtype_and_complement (S : hsubtype X) : ∏ x, S x -> subtype_complement S x -> empty.
proof: Proof. intros x in_S in_neg_S; exact (in_neg_S in_S). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions