Theoremsand_elim_left, and_elim_right, and_eq_false_eq_eq_false_or_eq_false, and_eq_true_eq_eq_true_and_eq_true, and_intro, and_le_left, and_le_right, apply_apply_apply, bne_eq_xor, bool_eq_false, bool_iff_false, coe_false, coe_sort_false, coe_sort_true, coe_true, coe_xor_iff, decide_congr, decide_false, decide_false_iff, decide_iff, decide_true, dichotomy, eq_false_eq_not_eq_true, eq_false_of_not_eq_true, eq_false_of_not_eq_true', eq_not_iff, eq_or_eq_not, eq_true_eq_not_eq_false, eq_true_of_not_eq_false, eq_true_of_not_eq_false', false_eq_true_eq_False, false_lt_true, injective_iff, le_and, le_iff_imp, left_le_or, lt_iff, ne_not, not_eq_false_eq_eq_true, not_eq_iff, not_eq_true_eq_eq_false, not_iff_not, not_ne_id, not_ne_self, ofNat_add_one, ofNat_le_ofNat, ofNat_toNat, ofNat_zero, of_decide_false, of_decide_true, or_eq_false_eq_eq_false_and_eq_false, or_eq_true_eq_eq_true_or_eq_true, or_inl, or_inr, or_le, right_le_or, self_ne_not, toNat_beq_one, toNat_beq_zero, toNat_bne_one, toNat_bne_zero, toNat_le_toNat, true_eq_false_eq_False, xor_iff_ne | 64 |