apply Iff.intro <;> intros h₃ <;> unfold FormalDual
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
⊢ F ∈ FormalDual Γ ↔ FormalDual Γ⊢F
case mp
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F

case mpr
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ