proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
proveit.logic.booleans.conjunction.left_from_and
proveit.logic.booleans.disjunction.unary_or_reduction
proveit.logic.sets.inclusion.relax_proper_subset
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
proveit.logic.sets.inclusion.unfold_subset_eq
proveit.numbers.addition.association
proveit.numbers.addition.disassociation
proveit.numbers.number_sets.complex_numbers.real_within_complex
proveit.numbers.number_sets.integers.nat_within_int
proveit.numbers.number_sets.rational_numbers.int_within_rational
proveit.numbers.number_sets.real_numbers.rational_within_real
proveit.numbers.numerals.decimals.add_1_1
proveit.numbers.numerals.decimals.nat1
proveit.numbers.numerals.decimals.nat2
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
proveit.core_expr_types.tuples.range_from1_len_is_nat
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
proveit.core_expr_types.tuples.extended_range_from1_len_typical_eq
proveit.core_expr_types.tuples.range_from1_len_typical_eq
proveit.logic.equality.sub_in_right_operands_via_tuple
proveit.numbers.addition.add_nat_closure_bin
proveit.logic.booleans.conjunction.some_from_and
proveit.logic.booleans.conjunction.any_from_and
proveit.logic.booleans.disjunction.binary_closure
proveit.logic.equality.sub_left_side_into
proveit.core_expr_types.tuples.merge_extension
proveit.logic.booleans.conjunction.and_if_both
proveit.numbers.number_sets.real_numbers.nat_pos_within_real