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

At: is member equalities lemma 1 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. 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)

false false
By: Rewrite (HigherC assert_evalC) 0
Generated subgoals:

None

About:
listboolbfalseassertapplyfunctionuniverseequalmemberimpliesall

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