fact: Fixpoint find_first (l: list A) : option nat := match l with | nil => None | hd::tl => match P_dec hd with | left _ => Some 0 | right _ => match find_first tl with | None => None | Some i => Some (S i) end end end.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)