(13steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: discrete equality is equivalence 1 4 1 2
1. T: Type
2. EQ: {T=}
3. EQ TT
4. x,y:T. EQ(x,y) x = y
5. x: T
6. y: T
7. EQ(y,x)
8. EQ(y,x) y = x
9. EQ(x,y) x = y
10. x = y y = x

EQ(x,y)
By: Repeat HypBackchain
Generated subgoals:

None

About:
boolassertapplyfunctionuniverseequalmemberall

(13steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc