Nuprl - Pf sublist list all lemma 1

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

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

L(eq)M (z:T. z(EQ) L z(eq) M)

By: Equivalence 3 THEN DiscreteEq 2 THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 3. EQ TT
4. x,y:T. EQ(x,y) x = y
5. eq: {T}
6. eq TT
7. x:T. eq(x,x)
8. x,y:T. eq(x,y) eq(y,x)
9. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
10. L: T List
11. M: T List
12. L(eq)M
z:T. z(EQ) L z(eq) M

2 3. EQ TT
4. x,y:T. EQ(x,y) x = y
5. eq: {T}
6. eq TT
7. x:T. eq(x,x)
8. x,y:T. eq(x,y) eq(y,x)
9. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
10. L: T List
11. M: T List
12. z:T. z(EQ) L z(eq) M
L(eq)M

About:

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

1	3. `EQ TT` 4. `x,y:T. EQ(x,y) x = y` 5. `eq:` `{T}` 6. `eq TT` 7. `x:T. eq(x,x)` 8. `x,y:T. eq(x,y) eq(y,x)` 9. `x,y,z:T. eq(x,y) eq(y,z) eq(x,z)` 10. `L:` `T List` 11. `M:` `T List` 12. `L(eq)M` `z:T. z(EQ) L z(eq) M`
2	3. `EQ TT` 4. `x,y:T. EQ(x,y) x = y` 5. `eq:` `{T}` 6. `eq TT` 7. `x:T. eq(x,x)` 8. `x,y:T. eq(x,y) eq(y,x)` 9. `x,y,z:T. eq(x,y) eq(y,z) eq(x,z)` 10. `L:` `T List` 11. `M:` `T List` 12. `z:T. z(EQ) L z(eq) M` `L(eq)M`