Proof of proveit.logic.sets.equivalence.set_equiv_reversal theorem

import proveit
from proveit import defaults
from proveit import A, B, x
from proveit.logic import And
from proveit.logic.sets import SetEquiv, SubsetEq
from proveit.logic.sets.equivalence  import set_equiv_def
theory = proveit.Theory() # the theorem's theory

%proving set_equiv_reversal

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

While this can be proven through automation, this manual proof is shorter and easy to follow.

A_equiv_B = set_equiv_reversal.condition

A_equiv_B:

defaults.assumptions = [A_equiv_B]

defaults.assumptions:

unfolded = A_equiv_B.unfold()

unfolded:  ⊢  

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

unfolded.instantiate().derive_reversed().generalize(x)

 ⊢  

%qed

proveit.logic.sets.equivalence.set_equiv_reversal has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , :
2	theorem		⊢
	proveit.logic.sets.equivalence.set_equiv_fold
3	generalization	4	⊢
4	instantiation	5, 6	⊢
	: , :
5	theorem		⊢
	proveit.logic.equality.equals_reversal
6	instantiation	7, 8	⊢
	: , :
7	theorem		⊢
	proveit.logic.sets.equivalence.set_equiv_unfold
8	assumption		⊢