Theorem: theoryValuationMonotone (Fine/SystemB/CanonicalModel.lean)

State before:
⊢ Monotone theoryValuation
Tactic:
intros _ _ h₁ n h₂
State after:
a✝ b✝ : Th
h₁ : a✝ ≤ b✝
n : ℕ
h₂ : n ∈ theoryValuation a✝
⊢ n ∈ theoryValuation b✝

State before:
a✝ b✝ : Th
h₁ : a✝ ≤ b✝
n : ℕ
h₂ : n ∈ theoryValuation a✝
⊢ n ∈ theoryValuation b✝
Tactic:
exact h₁ h₂
State after:
no goals