proveit.numbers.numerals.decimals.posnat2
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
proveit.logic.sets.intersection.membership_unfolding
proveit.logic.booleans.disjunction.or_if_left
proveit.logic.booleans.disjunction.or_if_both
proveit.logic.equality.lhs_via_equality