no goals
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝¹ : IsIrrefl α r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = EmptyRelation a b
simpa using not_rel_of_subsingleton r