added a test for rewrite under Pi

[helm.git] / matita / tests / rewrite.ma

diff --git a/matita/tests/rewrite.ma b/matita/tests/rewrite.ma
index c262613f226756ee0166f1ce2ba9d8dbd6958d9c..1321be02ca09cabf1208d7053ae98d8f39dc63aa 100644 (file)
--- 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.