rw [sillyLoop]
⊢ RTC SmallStep (sillyLoop, State.update "x" 1 fun x => 0) (Stmt.skip, fun x => 0)
⊢ RTC SmallStep
    (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)