fact: Fixpoint element_at (l : list A) (p : nat) : option A := match l with | nil => None | h :: t => match p with | 0 => Some h | S p' => element_at t p' end end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)