exact fun ⟨a, b, c⟩ => ⟨a, b.imp_right (H _), c⟩
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
no goals