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.