proposition: Lemma CPermutation_morph_cons : forall P : list A -> Prop, (forall a l, P (l ++ [a]) -> P (a :: l)) -> Proper (@CPermutation A ==> iff) P.
proof: Proof. enough (forall P : list A -> Prop, (forall a l, P (l ++ [a]) -> P (a :: l)) -> forall l1 l2, CPermutation l1 l2 -> P l1 -> P l2) as Himp by now intros P HP l1 l2 HC; split; [ | symmetry in HC ]; apply Himp. intros P HP l1 l2 [l1' l2']. revert l1'; induction l2' using rev_ind; intros l1' HPl. - now rewrite app_nil_r in HPl. - rewrite app_assoc in HPl. apply HP in HPl. rewrite <- app_assoc, <- app_comm_cons, app_nil_l. now apply IHl2'. Qed.
imports: List Permutation Morphisms PeanoNat