proveit.core_expr_types.conditionals.condition_prepend_reduction
proveit.logic.booleans.forall_over_bool_by_cases
proveit.logic.booleans.quantification.universality.bundle
proveit.logic.equality.equals_reversal
proveit.numbers.numerals.decimals.nat2
proveit.numbers.numerals.decimals.posnat1
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
proveit.logic.booleans.conditioned_forall_over_bool_by_cases
proveit.logic.booleans.false_eq_false
proveit.logic.booleans.implication.false_iff_true_negated
proveit.logic.booleans.implication.falsified_antecedent_implication
proveit.logic.booleans.implication.true_iff_false_negated
proveit.logic.booleans.true_eq_true