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

State before:
⊢ ∀ (Γ : Th), Monotone (formalApplicationFunction Γ)
Tactic:
intros Γ _ _ h₁
State after:
Γ a✝ b✝ : Th
h₁ : a✝ ≤ b✝
⊢ formalApplicationFunction Γ a✝ ≤ formalApplicationFunction Γ b✝

State before:
Γ a✝ b✝ : Th
h₁ : a✝ ≤ b✝
⊢ formalApplicationFunction Γ a✝ ≤ formalApplicationFunction Γ b✝
Tactic:
exact formalAppMonotoneLeft Γ h₁
State after:
no goals