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