proposition: Lemma Perm_list_eq_commute (x y y': list A): Permutation x y → list_eq y y' → exists x', list_eq x x' ∧ Permutation x' y'.
proof: Proof. Proof with simpl; intuition. intro P. revert y'. induction P. destruct y'... exists nil... destruct y'; simpl. intuition. intros [? Rxa]. destruct (IHP y' Rxa) as [x0[??]]. exists (a :: x0). intuition. destruct y'... destruct y'... exists (a0 :: a :: y'). intuition. apply perm_swap. intros. destruct (IHP2 y' H) as [?[??]]. destruct (IHP1 x H0) as [?[??]]. exists x0... transitivity x... Qed.
imports: Coq.Lists.List Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms CoRN.stdlib_omissions.Pair