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