proposition: Theorem split_one_permutation : forall (a : A) (l1 l2 : list A), In (a, l1) (split_one l2) -> Permutation (a :: l1) l2.
proof: Proof. intros a l1 l2; generalize a l1; elim l2; clear a l1 l2; simpl in |- *; auto. intros a l1 H1; case H1. intros a l H a0 l1 [H0| H0]. injection H0; intros H1 H2; rewrite H2, H1; auto. generalize H H0; elim (split_one l); simpl in |- *; auto. intros H1 H2; case H2. intros a1 l0 H1 H2 [H3| H3]; auto. injection H3; intros H4 H5; (rewrite <- H4, <- H5). apply perm_trans with (a :: fst a1 :: snd a1); auto. apply perm_skip. apply H2; auto. case a1; simpl in |- *; auto. Qed.
imports: List ListAux