import proveit
from proveit import defaults
theory = proveit.Theory() # the theorem's theory
%proving set_not_equiv_contradiction
defaults.assumptions = set_not_equiv_contradiction.all_conditions()
A_not_equiv_B = defaults.assumptions[1]
not_A_equiv_B = A_not_equiv_B.unfold()
not_A_equiv_B.derive_contradiction()
%qed