see dependencies
import proveit
from proveit.logic.sets.inclusion import subset_eq_def
%proving fold_subset_eq
subset_eq_def
subset_eq_def_inst = subset_eq_def.instantiate()
subset_eq_def_inst.derive_left_via_equality(assumptions=[subset_eq_def_inst.rhs])
%qed