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

At: discrete equality properties

T:Type, eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT
By:
Unfold `discrete_equality` 0
THEN
UnivCD
THEN
Analyze -1
Generated subgoal:

11. T: Type
2. eq: TT
3. x,y:T. eq(x,y) x = y
(x,y:T. eq(x,y) x = y) & eq TT

About:
boolassertapplyfunctionuniverseequalmemberandall

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