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

At: discrete equality symmetric 1 1
1. T: Type
2. eq: TT
3. (x,y:T. eq(x,y) x = y) & eq TT
4. x: T
5. y: T
6. eq(x,y)

eq(y,x)
By:
Analyze 3
THEN
HypBackchain
Generated subgoals:

None

About:
boolassertapplyfunctionuniverseequalmemberandall

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