Added faithfulness of the inclusion functor
	modified:   Splits.agda