Nuprl - Pf append commutes under is member

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

T:Type, eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) (M @ L)

By: UnivCD THEN Equivalence 2 THEN Repeat (Analyze 0)

Generated subgoals:

1 1. T: Type
2. eq: {T}
3. eq TT
4. x:T. eq(x,x)
5. x,y:T. eq(x,y) eq(y,x)
6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7. L: T List
8. M: T List
9. x: T
10. x(eq) (L @ M)
x(eq) (M @ L)

2 1. T: Type
2. eq: {T}
3. eq TT
4. x:T. eq(x,x)
5. x,y:T. eq(x,y) eq(y,x)
6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7. L: T List
8. M: T List
9. x: T
10. x(eq) (M @ L)
x(eq) (L @ M)

About:

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

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