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

case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ coRel r x y