Nuprl - Pf maction

1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. L1: Alph*
5. L2: Alph*
6. L: Alph*
7. (S:L1s) = (S:L2s)

(S:L @ L1s) = (S:L @ L2s)

By: ListInd 6

Generated subgoals:

1 (S:nil @ L1s) = (S:nil @ L2s)

2 8. u: Alph
9. v: Alph*
10. (S:v @ L1s) = (S:v @ L2s)
(S:(u.v) @ L1s) = (S:(u.v) @ L2s)

About:

1	`(S:nil @ L1s) = (S:nil @ L2s)`
2	8. `u:` `Alph` 9. `v:` `Alph*` 10. `(S:v @ L1s) = (S:v @ L2s)` `(S:(u.v) @ L1s) = (S:(u.v) @ L2s)`