proposition: Lemma lem_perm_3 : forall (x y : nat) l1 l2 l3, Permutation (x :: l1) l2 -> Permutation (x :: y :: l1 ++ l3) (y :: l2 ++ l3).
proof: Proof. srun eauto use: @lem_perm_1, Permutation_sym. Qed.
imports: Hammer(Hammer) Arith Sorting.Permutation