case axL _ _ _ _ => simp[Rew.rel, Rew.nrel]
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ CutRestricted C (id (Derivation.axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i)))
no goals