proveit.logic.sets.equivalence.set_equiv_reversal
proveit.logic.booleans.implication.modus_tollens_denial
proveit.logic.sets.equivalence.set_equiv_is_bool
proveit.logic.equality.sub_left_side_into