fact: Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n := match p with | @Fin.F1 k => fun v': t A (S k) => caseS' v' _ (fun h t => a :: t) | @Fin.FS k p' => fun v' : t A (S k) => (caseS' v' (fun _ => t A (S k)) (fun h t => h :: (replace t p' a))) end v.
imports: Arith_base