constructor
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y ↔ asymRel r x y
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y → asymRel r x y

case mpr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ asymRel r x y → coRel r x y