proposition: Lemma suffix_incl : forall l l' : list A, suffix l l' -> incl l l'.
proof: Proof. intros. apply incl_rev_intro. unfold suffix in H. apply prefix_incl. hyp. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)