apply BigStep.while_true
⊢ (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) ⟹
    fun x => 0
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"

case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State