-- Nomal CodeGear
whileLoop' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc)
  → (n ≡ varn env)
  → (next : Envc → t)
  → (exit : Envc → t) → t
whileLoop' zero env refl _ exit = exit env
whileLoop' (suc n) env refl next _ = next (record env {varn = pred (varn env) ; vari = suc (vari env) })

-- Hoare Logic base CodeGear
whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc )
  → (n ≡ varn env) → (pre : varn env + vari env ≡ c10 env)
  → (next : (env : Envc ) → (pred n ≡ varn env) → (post : varn env + vari env ≡ c10 env) → t)
  → (exit : (env : Envc ) → (fin : vari env ≡ c10 env)  → t) → t
whileLoopPwP' zero env refl refl next exit = exit env refl
whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))