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

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

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