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