Iso between RestFuns in completeness theorem
	modified:   Completeness.agda