1 subgoal
  
  x3 : nat
  ============================
   forall x x1 x4 x0 : nat,
   (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
1 subgoal
  
  x3 : nat
  x : nat
  x1 : nat
  x4 : nat
  x0 : nat
  H : forall x5 x6 : nat, x5 + x1 = x4 + x6
  ============================
   x + x1 = x4 + x0
1 subgoal
  
  x3 : nat
  ============================
   forall x x1 x4 x0 : nat,
   (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
   x + x1 = x4 + x0 -> foo (S x)
1 subgoal
  
  x3 : nat
  ============================
   forall x x1 x4 x0 : nat,
   (forall x2 x5 : nat,
    x2 + x1 = x4 + x5 ->
    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
   x + x1 = x4 + x0 ->
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
  
  x3 : nat
  x : nat
  x1 : nat
  x4 : nat
  x0 : nat
  ============================
   (forall x2 x5 : nat,
    x2 + x1 = x4 + x5 ->
    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
   x + x1 = x4 + x0 ->
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
  
  x3 : nat
  x : nat
  x1 : nat
  x4 : nat
  x0 : nat
  H : forall x5 x6 : nat,
      x5 + x1 = x4 + x6 ->
      forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)
  H0 : x + x1 = x4 + x0
  ============================
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
  
  x3 : nat
  x : nat
  x1 : nat
  x4 : nat
  x0 : nat
  H : forall x5 x6 : nat,
      x5 + x1 = x4 + x6 ->
      forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)
  H0 : x + x1 = x4 + x0
  x5 : nat
  x6 : nat
  x7 : nat
  S : nat
  ============================
   x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
  
  x3 : nat
  a : nat
  H : a = 0 -> forall a0 : nat, a0 = 0
  ============================
   a = 0