proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
proveit.core_expr_types.tuples.range_from1_len_typical_eq
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
proveit.core_expr_types.tuples.tuple_portion_substitution
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
proveit.numbers.addition.elim_zero_left
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.nat1
proveit.numbers.numerals.decimals.nat2
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
proveit.logic.booleans.conjunction.and_if_both
proveit.logic.equality.lhs_via_equality
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.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.core_expr_types.tuples.merge_extension
proveit.logic.equality.sub_right_side_into