import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.disjunction import true_or_false
theory = proveit.Theory() # the theorem's theory
%proving or_if_only_left
defaults.assumptions = or_if_only_left.all_conditions()
AeqT = A.evaluation()
BeqF = B.evaluation()
true_or_false
AorF = AeqT.sub_left_side_into(true_or_false, auto_simplify=False)
TorF = BeqF.sub_left_side_into(AorF, auto_simplify=False)
%qed