proposition: Theorem getAllPermutations_pred : forall (A B : Set)(R : A -> B -> Prop)(lsa : list A)(lsb : list B), list_pred R lsa lsb -> list_pred (list_pred R) (getAllPermutations lsa) (getAllPermutations lsb).
proof: Proof. induction 1; intuition; simpl in *. econstructor. econstructor. econstructor. eapply list_pred_flatten_both. eapply list_pred_map_both'. eapply list_pred_impl. eauto. intuition. eapply addInAllLocations_pred; intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation