import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.disjunction import false_or_true
theory = proveit.Theory() # the theorem's theory
%proving or_if_only_right
defaults.assumptions = or_if_only_right.all_conditions()
AeqF = A.evaluation()
BeqT = B.evaluation()
false_or_true
AorT = AeqF.sub_left_side_into(false_or_true, auto_simplify=False)
ForT = BeqT.sub_left_side_into(AorT, auto_simplify=False)
%qed