fact: Fixpoint put {n : nat} (f : fin n) (t : T) : vector T n -> vector T n := match f in fin n return vector T n -> vector T n with | F0 _ => fun v => Vcons t (vector_tl v) | FS _ f => fun v => Vcons (vector_hd v) (put f t (vector_tl v)) end.
imports: ExtLib.Data.Fin