Nuprl - Pf list iso weakening wrt identity 1

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

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

L(~eq)M

By: Equivalence 3 THEN HypSubst -1 0 THEN UnfoldTopAb 0 THEN Analyze 0

Generated subgoals:

1 4. eq TT
5. x:T. eq(x,x)
6. x,y:T. eq(x,y) eq(y,x)
7. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
8. L: T List
9. M: T List
10. L = M
M(eq)M

2 4. eq TT
5. x:T. eq(x,x)
6. x,y:T. eq(x,y) eq(y,x)
7. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
8. L: T List
9. M: T List
10. L = M
M(eq)M

About:

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

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