{ apply RTC.head
  { apply SmallStep.seq_skip }
  { apply RTC.head
    { apply SmallStep.whileDo }
    { apply RTC.head
      { apply SmallStep.if_false
        simp }
      { simp
        apply RTC.refl } } } }
case hbc.hbc.hbc.hbc

⊢ RTC SmallStep
    (Stmt.skip; Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0))
    (Stmt.skip, fun x => 0)
no goals