Proof of proveit.logic.sets.inclusion.unfold_subset_eq_contrapositive theorem

import proveit
from proveit import x, A, B
from proveit.logic import Boolean, InSet, SubsetEq
from proveit.logic.sets.inclusion import unfold_subset_eq
theory = proveit.Theory() # the theorem's theory

%proving unfold_subset_eq_contrapositive

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

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

unfold_subset_eq

 ⊢  

unfold_subset_eq_spec = unfold_subset_eq.instantiate(
        {x:x}, assumptions=[SubsetEq(A, B), InSet(x, A)])

unfold_subset_eq_spec: ,  ⊢  

unfold_subset_eq_spec_as_imp = unfold_subset_eq_spec.as_implication(hypothesis=InSet(x,A))

unfold_subset_eq_spec_as_imp:  ⊢  

unfold_subset_eq_spec_as_imp.contrapose(assumptions=[InSet(InSet(x, A), Boolean)])

,  ⊢