trying to finish the completeness theorem.
	modified:   RestrictionCat.agda
	modified:   Splits.agda