From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 10 Mar 2007 22:58:31 +0000 (+0000)
Subject: added a test for rewrite under Pi
X-Git-Tag: make_still_working~6430
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3ba17709a3bc7314f16f457ec4839e293e07b79;p=helm.git

added a test for rewrite under Pi
---

diff --git a/helm/software/matita/tests/rewrite.ma b/helm/software/matita/tests/rewrite.ma
index c262613f2..1321be02c 100644
--- a/helm/software/matita/tests/rewrite.ma
+++ b/helm/software/matita/tests/rewrite.ma
@@ -62,3 +62,10 @@ theorem test_rewrite_in_hyp2:
  rewrite < plus_n_O in H H1 \vdash (? ? %).
  split; [ exact H | exact H1].
 qed.
+
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+theorem test_rewrite_under_pi: \forall x,y. x = O \to y = O \to x = x \to O = x.
+intros 3.
+rewrite > H in \vdash (? \to ? ? % % \to ? ? ? %).
+intros. reflexivity.
+qed.