Nuprl - Proof: seq cons wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: seq cons wf 1

1. A : Type
2. n :

3. x : A
4. xs :

(n-1)

A
5. i :

if i=

x else xs(i-1) fi

By:	SplitITE Concl

Generated subgoals:

None

About:

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