exact ⟨ihp _ hp, ihq _ hq⟩
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)
p✝ q✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
ihp : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝¹ → CutRestricted C (Derivation.rewrite a✝¹ f)
ihq : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
hp : CutRestricted C a✝¹
hq : CutRestricted C a✝
⊢ CutRestricted C (Derivation.rewrite a✝¹ f) ∧ CutRestricted C (Derivation.rewrite a✝ f)
no goals