proposition: Lemma Suffix_x_y_or_y_x : forall (l:list A) (x y:A), In x l -> In y l -> (exists s, Suffix (x::s) l /\ In y (x::s)) \/ (exists s, Suffix (y::s) l /\ In x (y::s)).
proof: Proof. intros. induction l. inversion H. case H; intro Hax. left. exists l. split. rewrite Hax. apply Suffix_l_l. rewrite <- Hax; assumption. case H0; intro Hay. right. exists l. split. rewrite Hay. apply Suffix_l_l. rewrite <- Hay; assumption. change (In x l) in Hax. change (In y l) in Hay. generalize (IHl Hax Hay); intro H1. case H1; intro. left. elim H2; intros. exists x0. destruct H3. split. apply Suffix_step; assumption. assumption. right. elim H2; intros. exists x0. destruct H3. split. apply Suffix_step; assumption. assumption. Qed.
imports: Coq(List) Coq(Arith)