Nuprl - Pf sublist iff assert sublist 2 1

1. T: Type
2. Discrete{T}
3. eq: {T}
4. L: T List
5. M: T List

L(eq)M (eq)(L,M)

By: MoveToConcl 5 THEN ListInd -1

Generated subgoals:

1 M:T List. nil(eq)M (eq)(nil,M)

2 5. u: T
6. v: T List
7. M:T List. v(eq)M (eq)(v,M)
M:T List. (u.v)(eq)M (eq)(u.v,M)

About:

1	`M:T List. nil(eq)M (eq)(nil,M)`
2	5. `u:` `T` 6. `v:` `T List` 7. `M:T List. v(eq)M (eq)(v,M)` `M:T List. (u.v)(eq)M (eq)(u.v,M)`