From 0d2e7e10be19352ae652df7891d725223f794bad Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Feb 2006 10:59:05 +0000 Subject: [PATCH] No longer valid comment removed. --- helm/matita/library/nat/permutation.ma | 2 -- 1 file changed, 2 deletions(-) diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma index 3e987e9e8..d71f4fd27 100644 --- a/helm/matita/library/nat/permutation.ma +++ b/helm/matita/library/nat/permutation.ma @@ -444,8 +444,6 @@ apply H2. cut (permut (invert_permut n f) n).unfold permut in Hcut. elim Hcut.apply H4.assumption. apply permut_invert_permut.assumption.assumption. -(* uffa: lo ha espanso troppo *) -change with (invert_permut n f (f (invert_permut n f m)) = invert_permut n f m). apply invert_permut_f. cut (permut (invert_permut n f) n).unfold permut in Hcut. elim Hcut.apply H2.assumption. -- 2.39.2