proposition: Theorem Permutation_Add_inv a l1 l2 : Permutation l1 l2 -> forall l1' l2', Add a l1' l1 -> Add a l2' l2 -> Permutation l1' l2'.
proof: Proof. revert l1 l2. refine (Permutation_ind_bis _ _ _ _ _). - inversion_clear 1. - intros x l1 l2 PE IH. intros. InvAdd; try finish_basic_perms PE. constructor. now apply IH. - intros x y l1 l2 PE IH. intros. InvAdd; try finish_basic_perms PE. rewrite perm_swap; do 2 constructor. now apply IH. - intros l1 l l2 PE IH PE' IH' l1' l2' AD1 AD2. assert (Ha : In a l). { rewrite <- PE. rewrite (Add_in AD1). simpl; auto. } destruct (Add_inv _ _ Ha) as (l',AD). transitivity l'; auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat