cases hr with
| seq_step S S₂ _ _ s₂ hS₂ =>
  have hSs₁₂ :=
    ih hS₂
  aesop
| seq_skip => cases hS₁
case seq_step
Ss Ll : Stmt × State
S S₁ T : Stmt
s s₁ : State
hS₁ : (S, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (S, s) ⇒ Rr → (S₁, s₁) = Rr
Rr : Stmt × State
hr : (S; T, s) ⇒ Rr
⊢ (S₁; T, s₁) = Rr
no goals