rintro rfl
α : Type u_1
β : Type u_2
r s✝ s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
s : Set α
⊢ s = ∅ → BijOn f s ∅
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅