cut (permut (invert_permut n f) n).unfold permut in Hcut.
elim Hcut.apply H4.assumption.
apply permut_invert_permut.assumption.assumption.
cut (permut (invert_permut n f) n).unfold permut in Hcut.
elim Hcut.apply H4.assumption.
apply permut_invert_permut.assumption.assumption.