import proveit
from proveit import A
from proveit.logic import Not
from proveit.logic.booleans import false_not_true
theory = proveit.Theory() # the theorem's theory
%proving untrue_from_negation
false_not_true
A_eq_F = Not(A).prove(assumptions=[Not(A)]).equate_negated_to_false()
A_untrue = A_eq_F.sub_left_side_into(false_not_true)
%qed