apply BigStep.seq
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t

case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, ?hbody.t) ⟹ ?t

case hbody.t

⊢ State