Nuprl - Pf sublist reflexive 1

1. T: Type
2. eq: {T=}
3. L: T List

L(eq)L

By: ListInd 3 THEN AbReduce 0

Generated subgoals:

1 4. u: T
5. v: T List
6. v(eq)v
if eq(u,u) true else u(eq) v fi

2 4. u: T
5. v: T List
6. v(eq)v
v(eq)(u.v)

About:

1	4. `u:` `T` 5. `v:` `T List` 6. `v(eq)v` `if eq(u,u) true else u(eq) v fi`
2	4. `u:` `T` 5. `v:` `T List` 6. `v(eq)v` `v(eq)(u.v)`