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

At: equivalence reflexive 1 1
1. T: Type
2. eq: {T}
3. 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)

u:T. eq(u,u)
By:
Analyze 0
THEN
Witness4 u
THEN
Trivial
Generated subgoals:

None

About:
boolassertapplyfunctionuniversememberimpliesall

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