Theorem: Relation.Quasiorder.rc_refl (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x : α
⊢ reflRel r x x
Tactic:
right
State after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x : α
⊢ x = x

State before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x : α
⊢ x = x
Tactic:
rfl
State after:
no goals