fact: Fixpoint nth_error (ectx : eval_ctxt) (n : nat) : option value := match ectx with | Empty_ctxt => None | Push_ctxt t e cs => match n with | 0 => Some (VAbs t e) | S m => nth_error cs m end end.
imports: List Arith Bool