]> matita.cs.unibo.it Git - helm.git/commitdiff
added a test for rewrite under Pi
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 10 Mar 2007 22:58:31 +0000 (22:58 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 10 Mar 2007 22:58:31 +0000 (22:58 +0000)
helm/software/matita/tests/rewrite.ma

index c262613f226756ee0166f1ce2ba9d8dbd6958d9c..1321be02ca09cabf1208d7053ae98d8f39dc63aa 100644 (file)
@@ -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.