import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.disjunction import false_or_false_negated
theory = proveit.Theory() # the theorem's theory
%proving neither_intro
defaults.assumptions = neither_intro.all_conditions()
AeqF = A.evaluation()
BeqF = B.evaluation()
false_or_false_negated
AorF = AeqF.sub_left_side_into(false_or_false_negated.inner_expr().operand.operands[0],
auto_simplify=False)
ForF = BeqF.sub_left_side_into(AorF, auto_simplify=False)
%qed