Nuprl - Pf is member equality strengthening lemma 1 1 1 1

(7steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: is member equality strengthening lemma 1 1 1 1

1. T: Type
2. equiv: {T}
3. eq: {T=}
4. u: T
5. L: T List
6. u(equiv) L
7. M: T List
8. N: T List
9. y: T
10. equiv(u,y)
11. L = (M @ (y.N))
12. (M,N:T List. L = (M @ (y.N))) y(eq) L

v:T. equiv(u,v) & v(eq) L

By: Analyze -1

Generated subgoals:

1 M,N:T List. L = (M @ (y.N))

2 12. y(eq) L
v:T. equiv(u,v) & v(eq) L

About:

(7steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

1	`M,N:T List. L = (M @ (y.N))`
2	12. `y(eq) L` `v:T. equiv(u,v) & v(eq) L`