proposition: Theorem update_permute : forall (X:Type) v1 v2 x1 x2 (m : partial_map X), x2 <> x1 -> (update (update m x2 v2) x1 v1) = (update (update m x1 v1) x2 v2).
proof: Proof. intros X v1 v2 x1 x2 m. unfold update. apply t_update_permute. Qed.
imports: Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Logic.FunctionalExtensionality