import proveit
from proveit.logic import And
from proveit import A, B, C
from proveit.logic.booleans import in_bool_if_true
from proveit.logic.booleans.conjunction import left_in_bool, right_in_bool
theory = proveit.Theory() # the theorem's theory
%proving any_from_and