proposition: Lemma update_shadow : forall A (m: partial_map A) v1 v2 x, update (update m x v1) x v2 = update m x v2.
proof: Proof. intros A m v1 v2 x1. unfold update. rewrite t_update_shadow. reflexivity. Qed.
imports: Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Logic.FunctionalExtensionality