fact: Fixpoint get {T} {n : nat} (f : fin n) : vector T n -> T := match f in fin n return vector T n -> T with | F0 n => fun v : T * vector T n => fst v | FS n f => fun v : T * vector T n => get f (snd v) end.
imports: ExtLib.Data.Fin