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

At: discrete equality is equivalence 1 3 1
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(x,y)
8. EQ(y,x) y = x
9. EQ(x,y) x = y

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

None

About:
boolassertapplyfunctionuniverseequalmemberall

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