proposition: Lemma prefix_app_right_right : forall l l' l'', prefix l l' -> prefix l (l' ++ l'').
proof: Proof. induction l; simpl; intros. trivial. destruct l'; simpl in *|-* . contr. split. tauto. apply IHl. tauto. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)