Theoremsexists, rotate, imp_left, imp_right, elim, imp_left, imp_right, intro, axiom_of_choice, by_cases, by_contradiction, choose_eq, choose_eq', prop_complete, some_specβ, and_forall_ne, eq_or_ne, forall_or_left, forall_or_right, ne_or_eq, not_forallβ, or_not_of_imp, rec_eq_cast, trans_ne, fst, snd, imp, imp, elim, out, mt, mtr, and, iff, imp, ne, ne_left, ne_right, not, not_left, not_right, or, swap, ne_of_notMem, ne_of_notMem', dite_eq_left_iff, dite_eq_right_iff, dite_ne_left_iff, dite_ne_right_iff, ite_eq_left_iff, ite_eq_right_iff, ite_ne_left_iff, ite_ne_right_iff, ne_or_ne, trans_eq, decidable_imp_symm, imp_symm, elim3, imp3, rotate, exists_iff, forall_iff, or, and_forall_ne, and_iff_not_or_not, and_or_imp, and_symm_left, and_symm_right, apply_diteβ, apply_ite_left, apply_iteβ, beq_eq_beq, beq_eq_decide, beq_ext, beq_ext_iff, bex_def, by_cases, by_contra, by_contradiction, cast_heq_iff_heq, congr_arg_heq, congr_arg_refl, congr_fun_congr_arg, congr_fun_rfl, congr_heq, congr_refl_left, congr_refl_right, dcongr_heq, dec_em, dec_em', dite_apply, dite_dite_comm, dite_eq_iff, dite_eq_iff', dite_eq_or_eq, dite_mem, dite_ne_left_iff, dite_ne_right_iff, dite_prop_iff_and, dite_prop_iff_or, em, em', eqRec_heq', eq_cast_iff_heq, eq_equivalence, eq_false_intro, eq_iff_eq_cancel_left, eq_iff_eq_cancel_right, eq_ite_iff, eq_or_ne, eq_true_intro, exists_and_exists_comm, exists_apply_eq, exists_apply_eq_apply', exists_apply_eq_apply2, exists_apply_eq_apply2', exists_apply_eq_apply3, exists_apply_eq_apply3', exists_exists_and_eq_and, exists_exists_and_exists_and_eq_and, exists_exists_eq_and, exists_exists_exists_and_eq, exists_iff_of_forall, exists_mem_of_exists, exists_mem_or, exists_mem_or_left, exists_of_exists_mem, exists_or_forall_not, exists_prop_of_false, exists_swap, existsβ_comm, fact_iff, forall_and_index, forall_and_index', forall_and_left, forall_and_right, forall_apply_eq_imp_iff', forall_cond_comm, forall_eq_apply_imp_iff', forall_imp_iff_exists_imp, forall_mem_comm, forall_or_exists_not, forall_or_left, forall_or_of_or_forall, forall_or_right, forall_prop_congr, forall_prop_congr', forall_swap, forall_true_iff, forall_true_iff', forall_true_left, forallβ_and, forallβ_imp, forallβ_or_left, forallβ_swap, forallβ_true_iff, forallβ_imp, forallβ_true_iff, heq_cast_iff_heq, heq_iff_exists_cast_eq, heq_iff_exists_eq_cast, heq_of_eq_cast, heq_rec_iff_heq, if_congr, if_ctx_congr, iff_eq_eq, iff_iff_and_or_not_and_not, iff_iff_not_or_and_or_not, iff_mpr_iff_true_intro, iff_not_comm, imp_and_neg_imp_iff, imp_congr_ctx_eq, imp_congr_eq, imp_forall_iff, imp_forall_iff_forall, imp_iff_not_or, imp_iff_or_not, imp_iff_right_iff, imp_or, imp_or', instCommutativeXor', instSubsingletonSubtype_mathlib, ite_and, ite_apply, ite_eq_iff, ite_eq_iff', ite_eq_or_eq, ite_ite_comm, ite_mem, ite_ne_left_iff, ite_ne_right_iff, ite_or, ite_prop_iff_and, ite_prop_iff_or, lawful_beq_subsingleton, mem_dite, mem_ite, ne_and_eq_iff_right, ne_of_eq_of_ne, ne_of_ne_of_eq, ne_or_eq, not_and_not_right, not_and_or, not_beq_of_ne, not_exists_mem, not_forall_not, not_forallβ, not_forallβ_of_existsβ_not, not_iff, not_iff_comm, not_iff_not, not_imp, not_imp_comm, not_imp_not, not_imp_self, not_ne_iff, not_or_of_imp, not_xor, of_not_imp, of_not_not, or_congr_left', or_congr_right', or_iff_not_and_not, or_not, or_not_of_imp, peirce, rec_heq_iff_heq, rec_heq_of_heq, xor_comm, xor_def, xor_false, xor_iff_iff_not, xor_iff_not_iff, xor_iff_not_iff', xor_iff_or_and_not_and, xor_not_left, xor_not_not, xor_not_right, xor_self, xor_true | 240 |