have ⟨g,h₃⟩ := h₂
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
⊢ A ∈ formalApplication Γ b
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
g : Form
h₃ : g ∈ a ∧ g⊃A ∈ Γ
⊢ A ∈ formalApplication Γ b