rw [H]
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₁.ctx.hyps
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₂.ctx.hyps