proposition: Lemma prefix_incl : forall l l' : list A, prefix l l' -> incl l l'.
proof: Proof. induction l; intros. apply incl_nil. destruct l'. pose (prefix_nil (a::l) H). inversion e. simpl in H. rewrite (proj1 H). unfold incl. simpl. intros. destruct H0. tauto. constructor 2. apply IHl; tauto. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)