1 goal
  
  z := 0 : nat
  ============================
  True