Nuprl - Pf is member equalities lemma 1 2

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

At: is member equalities lemma 1 2

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. f: {T}
8. f TT
9. x:T. f(x,x)
10. x,y:T. f(x,y) f(y,x)
11. x,y,z:T. f(x,y) f(y,z) f(x,z)
12. u1: T
13. v: T List
14. u(eq) v u(f) v

if eq(u,u1) true else u(eq) v fi if f(u,u1) true else u(f) v fi

By: GenConcl (eq(u,u1) = b) THEN BoolInd -2 THEN Rewrite (HigherC ifthenelse_evalC THENC TryC (HigherC assert_evalC)) 0 THEN Analyze 0

Generated subgoals:

1 15. eq(u,u1) = true
16. True
if f(u,u1) true else u(f) v fi

2 15. eq(u,u1) = false
16. u(eq) v
if f(u,u1) true else u(f) v fi

About:

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