fact: Fixpoint projn n {A} : prodn n A -> forall i, i<n -> A := match n as n return prodn n A -> forall i, i<n -> A with | 0 => fun xs i (hi : i<0) => False_rect _ (Nat.nlt_0_r hi) | S n' => fun xs i => match i as i return i<S n' -> A with | 0 => fun _ => fst xs | S i' => fun hi => projn (snd xs) (NatCompat.lt_S_n hi) end end.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)