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

At: discrete equality symmetric

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

11. T: Type
2. eq: {T=}
3. x: T
4. y: T
eq(x,y) eq(y,x)

About:
assertapplyuniverseall

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