fact: Fixpoint position_aux (i : nat) (x : A) (l : list A) : option nat := match l with | nil => None | y :: m => if beq x y then Some i else position_aux (S i) x m end.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)