Equiv iff equiv derivable In hypothesis

theorem equiv_iff_equiv_derivableIn_hypothesis {A B : Proposition Atom} :    A ≡[T] B ↔      ∀ (Γ : Ctx Atom) (C : Proposition Atom),      DerivableIn T ((insert A Γ) ⊢ C) ↔ DerivableIn T ((insert B Γ) ⊢ C) := by  constructor  · intro ⟨e⟩ Γ C    exact ⟨fun D => mapEquivHypothesis Γ e C D.some, fun E => mapEquivHypothesis Γ e.symm C E.some⟩  · intro h    rw [equiv_iff]    constructor    · exact (h ∅ B).mpr ⟨ass <| by grind⟩    · exact (h ∅ A).mp ⟨ass <| by grind⟩