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

⊢ RTC SmallStep
    (Stmt.ifThenElse (fun s => s "x" > s "y")
        ((Stmt.skip; 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))
        Stmt.skip,
      State.update "x" 1 fun x => 0)
    (Stmt.skip, fun x => 0)
no goals