From a3ba17709a3bc7314f16f457ec4839e293e07b79 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 10 Mar 2007 22:58:31 +0000 Subject: [PATCH] added a test for rewrite under Pi --- helm/software/matita/tests/rewrite.ma | 7 +++++++ 1 file changed, 7 insertions(+) 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. -- 2.39.2