proposition: Lemma Permutation_morph_transp A : forall P : list A -> Prop, (forall a b l1 l2, P (l1 ++ a :: b :: l2) -> P (l1 ++ b :: a :: l2)) -> Proper (@Permutation A ==> Basics.impl) P.
proof: Proof. intros P HT l1 l2 HP. enough (forall l0, P (l0 ++ l1) -> P (l0 ++ l2)) as IH by (intro; rewrite <- (app_nil_l l2); now apply (IH nil)). induction HP; intuition. rewrite <- (app_nil_l l'), app_comm_cons, app_assoc. now apply IHHP; rewrite <- app_assoc. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat