proposition: Theorem addInAllLocations_perm : forall (A : Type) x0 (a : A) ls2, In ls2 (addInAllLocations a x0) -> Permutation ls2 (a :: x0).
proof: Proof. induction x0; intuition; simpl in *. intuition; subst. eapply Permutation_refl. intuition; subst. eapply Permutation_refl. eapply in_map_iff in H0. destruct H0. intuition; subst. eapply perm_trans. 2:{ eapply perm_swap. } eapply perm_skip. eapply IHx0. trivial. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation