import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic import in_bool, Or
theory = proveit.Theory() # the theorem's theory
%proving or_if_right
defaults.assumptions = or_if_right.all_conditions()
AeqT_or_AeqF = in_bool(A).unfold(assumptions=[in_bool(A)])
AeqT = AeqT_or_AeqF.operands[0]
AeqF = AeqT_or_AeqF.operands[1]
By proving $\vdash (B = \top) \in \mathbb{B}$ and $\vdash (B = \bot) \in \mathbb{B}$ (under no assumptions) we can force the proof to be shorter than otherwise (since it automatically deduces these assuming $B \in \mathbb{B}$ in a convoluted manner).
in_bool(AeqT).prove(assumptions=[])
in_bool(AeqF).prove(assumptions=[])
Or(A, B).prove(assumptions=[AeqT, B])
Or(A, B).prove(assumptions=[AeqF, B])
AeqT_or_AeqF.derive_via_singular_dilemma(Or(A, B), assumptions=[in_bool(A), B])
%qed