cases hS₁
case seq_step.seq_skip
Ss Ll : Stmt × State
S₁ T : Stmt
s s₁ : State
hS₁ : (Stmt.skip, s) ⇒ (S₁, s₁)
ih : ∀ {Rr : Stmt × State}, (Stmt.skip, s) ⇒ Rr → (S₁, s₁) = Rr
⊢ (S₁; T, s₁) = (T, s)
no goals