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

At: discrete equality reflexive

T:Type, eq:{T=}, u:T. eq(u,u)
By: UnivCD
Generated subgoal:

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

About:
assertapplyuniverseall

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