proposition: Lemma update_cons_case : forall n v x l, update n v (x::l) = (If n = 0 then v::l else x::(update (n-1) v l)).
proof: Proof. Proof using. intros. destruct n as [|n']; case_if. { applys update_zero. } { rewrite update_cons. fequals_rec. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)