1 files changed, 83 insertions, 0 deletions
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
new file mode 100644
index 00000000..105940a4
--- /dev/null
+++ b/test-suite/output/Naming.out
@@ -0,0 +1,83 @@
+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 x x3 : nat, x + x1 = x4 + x3
+  ============================
+   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 x x3 : nat,
+      x + x1 = x4 + x3 ->
+      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + 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 x x3 : nat,
+      x + x1 = x4 + x3 ->
+      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + 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 a : nat, a = 0
+  ============================
+   a = 0