proveit.logic.booleans.disjunction.binary_or_contradiction