proveit.logic.sets.equivalence.set_equiv_unfold
proveit.logic.equality.equals_reversal
proveit.logic.sets.equivalence.set_equiv_fold