proveit.logic.booleans.implication.eq_from_iff