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

At: equivalence 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

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