At: guarded prop to prop

  P:Prop, Q:Prop(given P). P  Q  Prop

1

1. P : Prop 2. Q : Prop(given P) 3. P   Q  Prop

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html