proposition: Theorem list_pred_nth_exists : forall (A B : Set)(P : A -> B -> Prop) lsa lsb, list_pred P lsa lsb -> forall n a, nth_option lsa n = Some a -> exists b, nth_option lsb n = Some b /\ P a b.
proof: Proof. induction 1; intuition; simpl in *. discriminate. destruct n. inversion H1; clear H1; subst. econstructor; intuition. edestruct IHlist_pred; eauto. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation