X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2Frewrite.ma;h=1321be02ca09cabf1208d7053ae98d8f39dc63aa;hb=fbdd1cc46819d19ed135391a4a954c19d1b92c0c;hp=c262613f226756ee0166f1ce2ba9d8dbd6958d9c;hpb=e9bc7577856e02545d3bc84d8f20aa15c5842034;p=helm.git

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.