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

At: discrete equality transitive

T:Type, eq:{T=}, x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
By: RepeatFor 5 (Analyze 0)
Generated subgoal:

11. T: Type
2. eq: {T=}
3. x: T
4. y: T
5. z: T
eq(x,y) eq(y,z) eq(x,z)

About:
assertapplyuniverseimpliesall

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