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

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:	MoveToConcl 6 THEN BifCase THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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