logo
In [1]:
import proveit
from proveit.logic.sets.inclusion  import proper_subset_def
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving unfold_proper_subset
Under these presumptions, we begin our proof of
unfold_proper_subset:
(see dependencies)
In [3]:
# pull in the proper subset definition
proper_subset_def
In [4]:
proper_subset_def_inst = proper_subset_def.instantiate()
proper_subset_def_inst:  ⊢  
In [5]:
proper_subset_def_inst.derive_right_via_equality(assumptions=[proper_subset_def_inst.lhs])
unfold_proper_subset may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [6]:
%qed
proveit.logic.sets.inclusion.unfold_proper_subset has been proven.
Out[6]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation2, 3, 4  ⊢  
  : , :
2theorem  ⊢  
 proveit.logic.equality.rhs_via_equality
3assumption  ⊢  
4instantiation5  ⊢  
  : , :
5axiom  ⊢  
 proveit.logic.sets.inclusion.proper_subset_def