proposition: Theorem allNats_nth_pred : forall (A : Set)(ls : list A), list_pred (fun (a : A) (b : nat) => nth_error ls b = Some a) ls (allNatsLt (length ls)).
proof: Proof. induction ls using rev_ind; intuition; simpl in *. econstructor. rewrite app_length. simpl. rewrite Nat.add_comm. simpl. eapply list_pred_app_both. eapply list_pred_impl. eapply IHls. intuition. eapply nth_error_app_Some; intuition. econstructor. eapply nth_error_app_length . econstructor. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation