rcases e with rfl
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
e : Δ = Γ
⊢ length (Derivation.cast d e) = length d
L : Language
Δ Δ₁ Δ₂ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d