proposition: Lemma update_cons_pos : forall n v x l, n > 0 -> update n v (x::l) = x::(update (n-1) v l).
proof: Proof. Proof using. introv N. rewrite update_cons_case. case_if. { false. math. } { auto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)