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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit import A
from proveit.logic import in_bool, Not
from proveit.logic.booleans.negation  import not_t, not_f
from proveit.logic.booleans.negation import double_negation_elim_lemma

%proving double_negation_elim

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

defaults.assumptions = double_negation_elim.conditions

defaults.assumptions:

double_negation_elim_lemma

 ⊢  

double_negation_elim_lemma.instantiate({A:A})

 ⊢  

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 8	⊢
	:
2	conjecture		⊢
	proveit.logic.booleans.negation.double_negation_elim_lemma
3	instantiation	5, 4	⊢
	:
4	instantiation	5, 6	⊢
	:
5	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
6	instantiation	7, 8	⊢
	:
7	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
8	assumption		⊢