import proveit
from proveit.numbers import num
from proveit import A, B, m
from proveit.logic.booleans.disjunction import multi_disjunction_def
theory = proveit.Theory() # the theorem's theory
%proving unary_or_lemma
multi_disjunction_def
multi_disjunction_def.instantiate({m:num(0), A:(), B:A})
%qed