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

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

%proving double_neg_closure

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

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

closure

 ⊢  

closure.instantiate({A:Not(A)}, assumptions=double_neg_closure.conditions)

 ⊢  

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	3, 2	⊢
	:
2	instantiation	3, 4	⊢
	:
3	conjecture		⊢
	proveit.logic.booleans.negation.closure
4	assumption		⊢