theorem
proved
PRCZeroCalibratedNativeCostCharacterTraceLiftTarget_proved
show as:
PRCZeroCalibratedNativeCostCharacterTraceLiftTarget_proved