proposition: Theorem permute_nth_equiv : forall (A : Set)(ls : list A) a b, list_pred (fun (a0 : A) (b0 : nat) => nth_error ls b0 = Some a0) a b -> a = permute ls b.
proof: Proof. induction a; inversion 1; intuition; simpl in *. subst. rewrite H2. f_equal. eapply IHa. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation