Nuprl Basics - Proof: sfa doc listind via so 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc listind via so 1 1

1. A : Type
2. Q : Prop
3. R : A

(A List)

Prop

Prop
4. x : A List

(Case of x; nil

Q ; a.x, rec:r

R(a,x,r))

Prop

By:	ListInd Hyp:-1 THEN Reduce Concl

Generated subgoals:

None

About:

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