proveit.logic.booleans.conjunction.false_and_true_negated
proveit.logic.equality.substitute_falsehood
proveit.logic.booleans.implication.negated_reflex
proveit.logic.equality.substitute_truth
proveit.logic.equality.sub_left_side_into