working with uniqueness of equality proofs of terms of type prop.
	modified:   PredicatePart.agda