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

State before:
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
Δ Γ : Sequent L
e : Δ = Γ
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.cast d e) ↔ CutRestricted C d
Tactic:
rcases e with ⟨rfl⟩
State after:
case refl
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
Δ : Sequent L
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.cast d ⋯) ↔ CutRestricted C d

State before:
case refl
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
Δ : Sequent L
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.cast d ⋯) ↔ CutRestricted C d
Tactic:
simp
State after:
no goals