proof: more fixes for the ERC20 proofs

Author: clarus

CoqOfRust/core/simulations/result.v

@@ -10,8 +10,8 @@ Module Result.
     Φ := Ty.apply (Ty.path "core::result::Result") [Φ A; Φ B];
     φ x :=
       match x with
-      | inl e => Value.StructTuple "core::result::Result::Err" [φ e]
-      | inr x => Value.StructTuple "core::result::Result::Ok" [φ x]
+      | inl x => Value.StructTuple "core::result::Result::Ok" [φ x]
+      | inr e => Value.StructTuple "core::result::Result::Err" [φ e]
       end;
   }.
 End Result.

CoqOfRust/examples/default/examples/ink_contracts/lib.v

@@ -50,5 +50,5 @@ Module Impl_Mapping_t_K_V.
 
   Axiom AssociatedFunction_insert :
     forall (K V : Ty.t),
-    M.IsAssociatedFunction (Self K V) "insert" (get K V).
+    M.IsAssociatedFunction (Self K V) "insert" (insert K V).
 End Impl_Mapping_t_K_V.