Isomorphism replaced with "if and only if"
	modified:   PredicatePart.agda