proveit.logic.sets.inclusion.subset_eq_reflexive
proveit.logic.equality.sub_right_side_into