import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.disjunction import true_or_true
theory = proveit.Theory() # the theorem's theory
%proving or_if_both
defaults.assumptions = or_if_both.all_conditions()
AeqT = A.evaluation()
BeqT = B.evaluation()
true_or_true
AorT = AeqT.sub_left_side_into(true_or_true.inner_expr().operands[0],
auto_simplify=False)
AorB = BeqT.sub_left_side_into(AorT, auto_simplify=False)
%qed