import proveit
theory = proveit.Theory() # the theorem's theory
%proving superset_membership_from_proper_subset
A_propersub_B = superset_membership_from_proper_subset.condition
A_propersub_B__unfolded = A_propersub_B.unfold(assumptions=[A_propersub_B])
A_sub_B = A_propersub_B__unfolded.derive_left()
%qed