no goals
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₁ : σ₁
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun a b => tr a = b) a₁ a₂ →
        match f₁ a₁ with
        | some b₁ => ∃ b₂, (fun a b => tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | none => f₂ a₂ = none) ↔
    FRespects f₂ tr (tr a₁) (f₁ a₁)
cases f₁ a₁ <;> simp only [FRespects, Respects, exists_eq_left', forall_eq']