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

At: discrete equality reflexive 1 1 1 1
1. T: Type
2. eq: TT
3. x,y:T. eq(x,y) x = y
4. u: T

eq(u,u)
By:
Witness3 u
THEN
With u (Analyze -1)
THEN
HypBackchain
Generated subgoal:

13. u: T
4. eq(u,u) u = u
u = u

About:
boolassertapplyfunctionuniverseequalall

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