proveit.logic.booleans.implication.eq_from_mutual_impl
proveit.logic.booleans.implication.iff_implies_left
proveit.logic.booleans.implication.iff_implies_right