apply SmallStep.seq_step
case hbc.hbc.hbc.hab

⊢ ((Stmt.assign "x" fun s => s "x" - 1);
        Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⇒
    ?hbc.hbc.hbc.b
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