Proof of proveit.logic.booleans.negation.double_negation_intro theorem

import proveit
from proveit import A
from proveit.logic import Not
theory = proveit.Theory() # the theorem's theory

%proving double_negation_intro

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
double_negation_intro:
(see dependencies)

double_negation_intro may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

not_a_eq_F = Not(A).evaluation(assumptions=[A])

not_a_eq_F:  ⊢  

not_a_eq_F.derive_via_boolean_equality()

 ⊢  

%qed # proven via automation

proveit.logic.booleans.negation.double_negation_intro has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	:
2	conjecture		⊢
	proveit.logic.booleans.negation.negation_intro
3	instantiation	4, 5, 6	⊢
	: , : , :
4	axiom		⊢
	proveit.logic.equality.equals_transitivity
5	instantiation	7, 8	⊢
	: , : , :
6	axiom		⊢
	proveit.logic.booleans.negation.not_t
7	axiom		⊢
	proveit.logic.equality.substitution
8	instantiation	9, 10	⊢
	:
9	axiom		⊢
	proveit.logic.booleans.eq_true_intro
10	assumption		⊢