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