proposition: Lemma R_two_prop : R 2 = Prop.
proof: Proof. ap extensionality; uhg; ir. rwi nat_realization_S H. nin H. rwi R_one_singleton_emptyset H. cp (singleton_eq H). rw H0. uf inc. sh False. rww R_false_emptyset. rwi R_one_singleton_emptyset H. rwi true_singleton_emptyset H. uhg; sh True. rw prop_realization; sy; am. apply by_cases with (B H). ir. assert (B H = True). ap iff_eq; ir. tv. am. assert (x = R True). wr H1. rww B_eq. rw nat_realization_S. ap or_intror. rw R_one_singleton_emptyset. wr R_true_singleton_emptyset. am. ir. assert (B H = False). ap iff_eq; ir. au. elim H1. rw nat_realization_S. ap or_introl. rw R_one_singleton_emptyset. assert (x = R (B H)). rww B_eq. rw H2. rw H1. rw R_false_emptyset. ap singleton_inc. Qed.
imports: tactics