From 3f2e93e2751e2bce2518502933b7169f99f2dbeb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 22 Aug 2005 08:43:01 +0000 Subject: [PATCH] Comment removed. --- helm/matita/tests/fguidi.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index a665ca85d..19f527e8f 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -46,7 +46,7 @@ intros. apply False_ind. cut (is_S O). auto paramodulation. elim H. exact I. qed. theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O). -intros. auto. (* paramodulation non trova la prova *) +intros. auto. qed. theorem eq_gen_S_S: \forall m,n. (S m) = (S n) \to m = n. -- 2.39.2