proveit.logic.booleans.negation.double_negation_elim_lemma
proveit.logic.booleans.in_bool_if_true