fact: Definition t_update {A : Type} (m : total_map A) (x : string) (v : A) := fun x' => if String.eqb x x' then v else m x'.
imports: Coq(Arith.Arith) Coq(Bool.Bool) Coq.Strings.String Coq(Logic.FunctionalExtensionality) Coq(Lists.List)