new version using prop (but I still have to remove "isomorphism as equality")
	modified:   PredicatePart.agda