60def Distinction (K : Type*) : Type _ := K → K → Prop
proof body
Definition body.
61 62/-- The canonical distinction induced by equality: two elements are 63distinct iff they are not equal. This is the most primitive distinction 64on any type and exists for every type without further structure. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.