fact: Fixpoint put {T} {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 => (t, snd v) | FS _ f => fun v => (fst v, put f t (snd v)) end.
imports: ExtLib.Data.Fin