No longer valid comment removed.

diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma
index 3e987e9e8c0df185f4c2a48271fef43dee2a2a1d..d71f4fd27a2690b14358c9fb035ef83cdb451b55 100644 (file)
--- 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.