proposition: Theorem list_pred_nth : forall n (A B : Set) P (lsa : list A)(lsb : list B) defa defb, list_pred P lsa lsb -> P defa defb -> P (nth n lsa defa) (nth n lsb defb).
proof: Proof. induction n; intuition; simpl in *. inversion H; clear H; subst; intuition; simpl in *. inversion H; clear H; subst; intuition; simpl in *. eapply IHn; intuition. Qed.
imports: FCF.FCF Permutation