proposition: Theorem getAllPerms_permute_eq : forall (A : Set)(ls : list A), list_pred (fun (a : list A) (b : list nat) => a = permute ls b) (getAllPermutations ls) (getAllPermutations (allNatsLt (length ls))).
proof: Proof. intuition. generalize (@getAllPermutations_pred _ _ (fun a b => nth_error ls b = Some a) ls (allNatsLt (length ls))) ; intros. eapply list_pred_impl. eapply H. eapply allNats_nth_pred. intuition. eapply permute_nth_equiv. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation