import proveit
from proveit.logic import TRUE, FALSE
from proveit import A
from proveit.logic.booleans.disjunction import unary_or_lemma
from proveit.logic.booleans.disjunction import or_f_t, or_f_f
theory = proveit.Theory() # the theorem's theory
%proving unary_or_reduction
base_case_t_r_u_e = unary_or_lemma.instantiate({A:TRUE})
base_case_f_a_l_s_e = unary_or_lemma.instantiate({A:FALSE})
base_case_t_r_u_e.sub_left_side_into(or_f_t)
base_case_f_a_l_s_e.sub_left_side_into(or_f_f)
%qed