fact: Fixpoint greatest_nodup_prefix_aux (acc l : list A) : list A := match l with | nil => rev acc | cons x l => match In_dec eq_dec x acc with | left _ => rev acc | right _ => greatest_nodup_prefix_aux (x :: acc) l end end.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)