proveit.logic.booleans.implication.iff_f_t
proveit.logic.booleans.negation.negation_intro