proveit.logic.equality.sub_right_side_into
proveit.logic.sets.enumeration.unfold
proveit.numbers.numerals.decimals.nat2
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq