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