proposition: Lemma list_pred_allNatsLt : forall (A : Set)(ls : list A), list_pred (fun i a => forall a', nth i ls a' = a) (allNatsLt (length ls)) ls.
proof: Proof. induction ls using rev_ind; intuition; simpl in *. econstructor. rewrite app_length. rewrite Nat.add_comm. simpl. eapply list_pred_rev. eapply list_pred_impl'. eapply IHls. intuition. rewrite app_nth1. eauto. apply allNatsLt_lt. trivial. intuition. rewrite app_nth2. rewrite Nat.sub_diag. simpl. trivial. intuition. Qed.
imports: FCF.FCF Permutation