Nuprl - Proof: list iso 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list iso 2 1 1 1 1

1. 'a : S
2. x' : 'a List
3. x'' : 'a List
4. (

. if n<

||x'|| then x'[n] else arb('a) fi )
4. =
4. (

. if n<

||x''|| then x''[n] else arb('a) fi )
5. ||x'|| = ||x''||

(

||x'||. x'[i]){

||x'||} = (

||x''||. x''[i]){

||x''||}

By:	Analyze THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 (i:||x'||. x'[i]) = (i:||x''||. x''[i]) ||x'||'a
4 steps

About:

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