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