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