1 subgoal
  
  z := 0 : nat
  ============================
  True