simp only [vars, List.mem_bind, List.mem_cons, H₂]
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ v ∈ vars s₁ → v ∈ vars s₂
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ (∃ a, (a = s₂.fmla ∨ a ∈ s₁.ctx.hyps) ∧ v ∈ Expr.vars a.snd) →
    ∃ a, (a = s₂.fmla ∨ a ∈ s₂.ctx.hyps) ∧ v ∈ Expr.vars a.snd