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

At: equivalence reflexive

T:Type, eq:{T}, u:T. eq(u,u)
By:
Analyze 0
THEN
Analyze 0
Generated subgoal:

11. T: Type
2. eq: {T}
u:T. eq(u,u)

About:
assertapplyuniverseall

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