import proveit
from proveit import A, B
from proveit.logic.sets.inclusion import proper_subset_def
theory = proveit.Theory() # the theorem's theory
%proving fold_proper_subset
# pull in the proper subset definition
proper_subset_def
proper_subset_def_inst = proper_subset_def.instantiate()
proper_subset_def_inst_derive_left = proper_subset_def_inst.derive_left_via_equality(
assumptions=[proper_subset_def_inst.rhs])
proper_subset_def_inst_derive_left.generalize(
[[A, B]], conditions=[*proper_subset_def_inst_derive_left.assumptions])
%qed