{ apply RTC.head
  { apply SmallStep.seq_step
    apply SmallStep.assign }
  { 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

⊢ RTC SmallStep
    ((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)
    (Stmt.skip, fun x => 0)
no goals