see dependencies
import proveit
from proveit import A, B
from proveit.logic.sets.inclusion import subset_eq_def
%proving unfold_subset_eq
subset_eq_def
SubsetEqDef_inst = subset_eq_def.instantiate()
SubsetEqDef_inst.derive_right_via_equality(assumptions=[SubsetEqDef_inst.lhs])
%qed