NT253 (Click "Prove" to run)

Prove:


   Proof Trace