proposition: Theorem addInAllLocations_pred : forall (A B : Set) (R : A -> B -> Prop) (a : list A) (b : list B), list_pred R a b -> forall a1 a2, R a1 a2 -> list_pred (list_pred R) (addInAllLocations a1 a) (addInAllLocations a2 b).
proof: Proof. induction 1; intuition; simpl in *. econstructor. econstructor. trivial. econstructor. econstructor. econstructor. repeat econstructor;assumption. eapply list_pred_map_both'. eapply list_pred_impl. eauto. intuition. econstructor; assumption. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation