Theorem: LO.FirstOrder.Derivation.CutRestricted.ex' (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d :  ⊢¹ [→ t].hom p :: Δ
⊢ CutRestricted C (Derivation.ex t d) → CutRestricted C d
Tactic:
rintro ⟨⟩
State after:
case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d :  ⊢¹ [→ t].hom p :: Δ✝
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d

State before:
case ex
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d :  ⊢¹ [→ t].hom p :: Δ✝
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d
Tactic:
assumption
State after:
no goals