proposition: Lemma Suffix_In : forall s l:list A, Suffix s l -> (forall x:A, In x s -> In x l).
proof: Proof. intros s l Hsuff x Hs. elim Hsuff. intros p Heq. rewrite <- Heq. intuition auto with datatypes. Qed.
imports: Coq(List) Coq(Arith)