proposition: Lemma not_empty_nonemptyT : forall x : E, ~ empty x -> nonemptyT x.
proof: Proof. ir. ap excluded_middle. unfold not in |- *. ir. unfold not in H. ap H. unfold empty in |- *. unfold not in |- *. ir. ap H0. ap nonemptyT_intro. exact (B H1). Qed.
imports: tactics