fact: Fixpoint tail_nth (l : list A) (n : nat) : option (list A) := match l, n with | _, 0 => Some l | a :: l', S n' => tail_nth l' n' | _, _ => None end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)