theorem
proved
PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_iff_mixed_reflects
show as:
PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_iff_mixed_reflects