fact: Fixpoint replace_Index {m} (As : Vector.t A m) (il : ilist As) (n : Fin.t m) (new_b : B (Vector.nth As n)) {struct n} : ilist As := match n in Fin.t m return forall (As : Vector.t A m), @ilist _ B _ As -> B (Vector.nth As n) -> ilist As with | Fin.F1 k => fun As => Vector.caseS (fun n As => ilist As -> B (Vector.nth As (@Fin.F1 n)) -> ilist As) (fun h n t il new_b => icons new_b (ilist_tl il) ) As | Fin.FS k n' => fun As => Vector_caseS' Fin.t (fun n As n' => ilist As -> B (Vector.nth As (@Fin.FS n n')) -> ilist As) (fun h n t m il new_b => icons (ilist_hd il) (@replace_Index _ _ (ilist_tl il) _ new_b)) As n' end As il new_b.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common Fiat.Common.VectorFacts