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

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

%proving subset_eq_reflexive

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

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

%qed

proveit.logic.sets.inclusion.subset_eq_reflexive has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , : , :
2	theorem		⊢
	proveit.logic.sets.inclusion.fold_subset_eq
3	generalization	4	⊢
4	assumption		⊢