1 goal
  
  x : nat
  ============================
  x = S x
1 goal
  
  x : nat
  ============================
  0 + x = S x
1 goal
  
  x : nat
  ============================
  x = 1 + x