proposition: Lemma map_update : forall n f l x, n < length l -> map f (update n x l) = update n (f x) (map f l).
proof: Proof. Proof using. introv I. gen n. induction l; intros; rew_list in *. { false; math. } { destruct n as [|n']. { rewrite~ update_zero. } { rewrite map_cons. do 2 rewrite update_cons. rewrite map_cons. fequals. applys IHl. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)