proposition: Theorem permutation_inv : forall (a : A) (l1 l2 : list A), permutation (a :: l1) (a :: l2) -> permutation l1 l2.
proof: Proof. intros a l1 l2 H; case permutation_cons_ex with (1 := H). intros l3 (l4, (Hl1, Hl2)). apply permutation_trans with (1 := Hl2). generalize Hl1; case l3; simpl in |- *; auto. intros H1; injection H1; intros H2; rewrite H2; auto. intros a0 l5 H1; injection H1; intros H2 H3; rewrite H2; rewrite H3; auto. apply permutation_trans with (a0 :: l4 ++ l5); auto. apply permutation_skip; apply permutation_app_swap. apply (permutation_app_swap (a0 :: l4) l5). Qed.
imports: List ListAux