theorem
proved
PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_iff_prime_identity_iff_two
show as:
PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_iff_prime_identity_iff_two