proposition: Lemma update_zero : forall v x l, (x::l)[0:=v] = v::l.
proof: Proof. Proof using. intros. unfold update, update_inst, update_impl. case_if. false; math. rewrite~ update_zero. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)