proposition: Lemma suffix_cut : forall (x : A) l, suffix (cut x l) l.
proof: Proof. unfold suffix. induction l; simpl; intros. trivial. destruct (eq_dec x a). rewrite <- e. apply reflexive_prefix. apply prefix_app_right_right. hyp. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)