rw [e]
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₁) x
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₂) x