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

At: discrete equality is equivalence 1 3
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)

EQ(y,x)
By:
CopyToEnd 4
THEN
With y (Analyze -1)
THEN
With x (Analyze -1)
THEN
CopyToEnd 4
THEN
With x (Analyze -1)
THEN
With y (Analyze -1)
Generated subgoal:

18. EQ(y,x) y = x
9. EQ(x,y) x = y
EQ(y,x)

About:
boolassertapplyfunctionuniverseequalmemberall

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