Nuprl - Proof: list iso 2 1 1 1 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 1 1

1. 'a : S
2. x' : 'a List
3. x'' : 'a List
4. ||x'|| = ||x''||
5. i :

||x'||
6. if i<

||x'|| then x'[i] else arb('a) fi
6. =
6. if i<

||x''|| then x''[i] else arb('a) fi

x'[i] = x''[i]

By:	H 4 6 THEN Simp THEN StrongAuto

Generated subgoal:

1 6. if i<||x''|| then x'[i] else arb('a) fi
6. =
6. if i<||x''|| then x''[i] else arb('a) fi
x'[i] = x''[i]
1 step

About:

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