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

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

EQ(x,x)
By:
Witness4 x
THEN
With x (Analyze -1)
THEN
HypBackchain
Generated subgoals:

None

About:
boolassertapplyfunctionuniverseequalmemberall

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