proposition: Theorem update_same : forall X v x (m : partial_map X), m x = Some v -> update m x v = m.
proof: Proof. intros X v x m H. unfold update. rewrite <- H. apply t_update_same. Qed.
imports: Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Logic.FunctionalExtensionality