fact: Fixpoint nth_finite (P:set) (k:nat) (PF : finite P) {struct PF}: (k < size PF) -> A := match PF as F return (k < size F) -> A with fin_eq_empty H => (fun (e : k<0) => match lt_n_O k e with end) | @fin_eq_add _ x Q nqx fq eqq => match k as k0 return k0<S (size fq)->A with O => fun e => x | (S k1) => fun (e:S k1<S (size fq)) => nth_finite fq (lt_S_n k1 (size fq) e) end end.
imports: Coq(Arith) Coq(Lt)