Theorem: formalAppMonotoneRight (Fine/SystemB/Theories.lean)

State before:
⊢ ∀ (Γ : Ctx), Monotone (flip formalApplication Γ)
Tactic:
intros Γ a b h₁ A h₂
State after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ flip formalApplication Γ a
⊢ A ∈ flip formalApplication Γ b

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

State before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ flip formalApplication Γ a
g : Form
h₃ : g ∈ Γ ∧ g⊃A ∈ a
⊢ A ∈ flip formalApplication Γ b
Tactic:
exact ⟨g, h₃.left, h₁ h₃.right⟩
State after:
no goals