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

At: discrete equality transitive 1
1. T: Type
2. eq: {T=}
3. x: T
4. y: T
5. z: T

eq(x,y) eq(y,z) eq(x,z)
By:
Analyze 2
THEN
Analyze 3
THEN
UnivCD
Generated subgoal:

12. eq: TT
3. x,y:T. eq(x,y) x = y
4. eq TT
5. x: T
6. y: T
7. z: T
8. eq(x,y)
9. eq(y,z)
eq(x,z)

About:
assertapplyuniverseimplies

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