aesop
case seq_step.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
S₂ : Stmt
s₂ : State
hS₂ : (S, s) ⇒ (S₂, s₂)
hSs₁₂ : (S₁, s₁) = (S₂, s₂)
⊢ (S₁; T, s₁) = (S₂; T, s₂)
no goals