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

At: equivalence symmetric 1

1. T: Type
2. eq: {T}
3. x: T
4. y: T

eq(x,y) eq(y,x)

By: Equivalence 2

Generated subgoal:

13. eq TT
4. x:T. eq(x,x)
5. x,y:T. eq(x,y) eq(y,x)
6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7. x: T
8. y: T
eq(x,y) eq(y,x)

About:
assertapplyuniverse

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