Nuprl - Pf sublist weakening wrt identity 1 1

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

L(eq)L

By: Analyze 4 THEN Rewrite (HigherC sublist_unrollC) 0 THEN Try Trivial

Generated subgoal:

1 7. u: T
8. v: T List
u(eq) (u.v) & v(eq)(u.v)

About: