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

At: discrete equality inc equivalence

T:Type. {T=} {T}
By:
Unfold `subtype` 0
THEN
UnivCD
Generated subgoal:

11. T: Type
2. x: {T=}
x {T}

About:
universemembersubtypeall

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