A tough test for rewrite.

diff --git a/helm/gTopLevel/esempi/rewrite.cic b/helm/gTopLevel/esempi/rewrite.cic
new file mode 100644 (file)
index 0000000..ff2b92e
--- /dev/null
+++ b/helm/gTopLevel/esempi/rewrite.cic
@@ -0,0 +1,5 @@
+!v:nat.(eq nat -> nat -> nat \x:nat.\y:nat.(plus y v) \x:nat.\y:nat.O)
+
+Fare cut di:
+ (eq nat -> nat \w:nat.(plus w v) \w:nat.(plus (plus w w) v))
+e poi riscriverlo