Extend the proof to a non-transparent port