proposition: Lemma Suffix_step : forall (x:A) (s l:list A), Suffix s l -> Suffix s (x::l).
proof: Proof. intros x s l Hsuff. unfold Suffix in * |- *. elim Hsuff. intros p Heq. exists (x::p). rewrite <- Heq. reflexivity. Qed.
imports: Coq(List) Coq(Arith)