proposition: Lemma CPermutation_Forall2 A B (P : A -> B -> Prop) : forall l1 l1' l2, CPermutation l1 l1' -> Forall2 P l1 l2 -> exists l2', CPermutation l2 l2' /\ Forall2 P l1' l2'.
proof: Proof. intros ? ? ? [? ?] HF. apply Forall2_app_inv_l in HF as (l2' & l2'' & HF' & HF'' & ->). exists (l2'' ++ l2'); intuition. now apply Forall2_app. Qed.
imports: List Permutation Morphisms PeanoNat