eq:{T
}, f:{T=}, x,y:T. 
eq(x,y) 
f(x,y)eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y)| Theorem | Name | ||
| Thm* eq:{T}, f:{T=}, x,y:T. eq(x,y) f(x,y) | [not_equivalence_implies_not_discrete_eq] | ||
| cites | |||
| Thm* eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y) | [equivalence_weakening_lemma] |