From f396728a5a99733b1d46a3d1f3cd07b68ede07ec Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 10 Mar 2007 22:58:31 +0000
Subject: [PATCH] added a test for rewrite under Pi

---
 matita/tests/rewrite.ma | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/matita/tests/rewrite.ma b/matita/tests/rewrite.ma
index c262613f2..1321be02c 100644
--- a/matita/tests/rewrite.ma
+++ b/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.
-- 
2.39.2