(6steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete equality properties 1 2 2
1. T: Type
2. eq: TT
3. x,y:T. eq(x,y) x = y
4. x: T
5. y: T
6. x = y

eq(x,y)
By: HypBackchain
Generated subgoals:

None

About:
boolassertapplyfunctionuniverseequalall

(6steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc