α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
b✝ b : α
⊢ r b b → r b b
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
a b : α
⊢ ∀ ⦃b : α⦄, b ∈ {a} → r a b → r b a
rintro b (rfl : b = a)
no goals
α : Type u_1
r r₁ r₂ : α → α → Prop
s t : Set α
b✝ b : α
⊢ r b b → r b b
exact id