proposition: Lemma true_singleton_emptyset : singleton emptyset = True.
proof: Proof. ap extensionality; uhg; ir. cp (singleton_eq H). rw H0. assert True. tv. cp (true_proof_emptyset H1). uf inc. sh H1. am. cp (true_proof_emptyset (B H)). rwi B_eq H0. rw H0. ap singleton_inc. Qed.
imports: tactics