proposition: Theorem permute_length_eq : forall (sigma : list nat)(ls : list A), (forall n, In n sigma -> n < length ls) -> length (permute ls sigma) = length sigma.
proof: Proof. induction sigma; intuition; simpl in *. case_eq (nth_error ls a); intuition. simpl. f_equal. eapply IHsigma; intuition. exfalso. eapply nth_error_not_None. eapply H. intuition. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation