proposition: Lemma update_ge_length : forall n v l, n >= length l -> update n v l = l.
proof: Proof. Proof using. introv E. gen n. induction l; rew_list; intros. { auto. } { rewrite update_cons_pos; [|math]. fequals. applys IHl. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)