apply SmallStep.assign
case hbc.hbc.hbc.hab.hS

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⇒ (?hbc.hbc.hbc.hab.S', ?hbc.hbc.hbc.hab.s')

case hbc.hbc.hbc.hab.S'

⊢ Stmt

case hbc.hbc.hbc.hab.s'

⊢ State
no goals