A:Type, P:(AType).
  (x:A. Dec(P(x)))  (!{p:(A)| x:A. p(x)  P(x) })

By:	Guarding (<type>) UnivCD THEN FwdThru:  Thm*  (x:T. Dec(E(x)))  (f:(T). x:T. f(x)  E(x)) on [ x:A. Dec(P(x)) ]

1

1. A : Type 2. P : AType 3. x:A. Dec(P(x)) 4. f:(A). x:A. f(x)  P(x)   !{p:(A)| x:A. p(x)  P(x) }

5 steps

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