proposition: Lemma prefix_smaller : forall (x : A) l l', l <> l'++x::nil -> prefix l (l'++x::nil) -> prefix l l'.
proof: Proof. induction l; intros. trivial. destruct l'. simpl in H0. destruct H0. pose (prefix_nil l H1). rewrite H0, e in H. tauto. simpl in H0. simpl. split. tauto. apply IHl. intro. rewrite (proj1 H0), H1 in H. tauto. tauto. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)