Nuprl - Pf is member equalities lemma

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

T:Type, eq:{T=}, u:T, L:T List. u(eq) L (f:{T}. u(f) L)

By: Analyze 0 THEN Analyze 0 THEN DiscreteEq -1 THEN UnivCD THEN Equivalence -1

Generated subgoal:

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

About:

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