(13steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
discrete
equality
is
equivalence
T:Type, EQ:{T=
}. EQ
{T
}
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
EQ:
{T=
}
EQ
{T
}
About:
(13steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
}
EQ 
{T
}
T:Type, EQ:{T=}. EQ {T}
} EQ {T}
