fact: Fixpoint update A (n:nat) (v:A) (l:list A) { struct l } : list A := match l with | nil => nil | x::l' => match n with | 0 => v::l' | S n' => x::update n' v l' end end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)