(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

(* StructRecord
  {
    name := "Mapping";
    const_params := [];
    ty_params := [ "K"; "V" ];
    fields :=
      [
        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ]);
        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ])
      ];
  } *)

Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_multisig_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "multisig::Mapping") [] [ K; V ].
  
  Parameter default : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    forall (K V : Ty.t),
    M.IsTraitInstance
      "core::default::Default"
      (Self K V)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method (default K V)) ].
End Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_multisig_Mapping_K_V.

Module Impl_multisig_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "multisig::Mapping") [] [ K; V ].
  
  Parameter contains : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_contains :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "contains" (contains K V).
  
  Parameter get : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_get :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "get" (get K V).
  
  Parameter insert : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_insert :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "insert" (insert K V).
  
  Parameter remove : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_remove :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "remove" (remove K V).
  
  Parameter size : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_size :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "size" (size K V).
  
  Parameter take : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_take :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "take" (take K V).
End Impl_multisig_Mapping_K_V.

(* StructTuple
  {
    name := "AccountId";
    const_params := [];
    ty_params := [];
    fields := [ Ty.path "u128" ];
  } *)

Module Impl_core_default_Default_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter default : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_AccountId.

Module Impl_core_fmt_Debug_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter fmt : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_multisig_AccountId.

Module Impl_core_clone_Clone_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter clone : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_multisig_AccountId.

Module Impl_core_marker_Copy_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_multisig_AccountId.

Module Impl_core_marker_StructuralPartialEq_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_multisig_AccountId.

Module Impl_core_cmp_PartialEq_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter eq : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_multisig_AccountId.

Module Impl_core_cmp_Eq_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter assert_receiver_is_total_eq : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_multisig_AccountId.

Module Impl_core_cmp_PartialOrd_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter partial_cmp : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialOrd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
End Impl_core_cmp_PartialOrd_for_multisig_AccountId.

Module Impl_core_cmp_Ord_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Parameter cmp : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Ord"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
End Impl_core_cmp_Ord_for_multisig_AccountId.

Axiom Balance : (Ty.path "multisig::Balance") = (Ty.path "u128").

(* StructRecord
  {
    name := "Env";
    const_params := [];
    ty_params := [];
    fields := [ ("caller", Ty.path "multisig::AccountId") ];
  } *)

Parameter value_MAX_OWNERS : Value.t.

Axiom TransactionId : (Ty.path "multisig::TransactionId") = (Ty.path "u32").

Parameter value_WRONG_TRANSACTION_ID : Value.t.

(* StructTuple
  {
    name := "CallInput";
    const_params := [];
    ty_params := [];
    fields := [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ];
  } *)

(*
Enum ConfirmationStatus
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Confirmed";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "ConfirmationsNeeded";
        item := StructTuple [ Ty.path "u32" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_clone_Clone_for_multisig_ConfirmationStatus.
  Definition Self : Ty.t := Ty.path "multisig::ConfirmationStatus".
  
  Parameter clone : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_multisig_ConfirmationStatus.

Module Impl_core_marker_Copy_for_multisig_ConfirmationStatus.
  Definition Self : Ty.t := Ty.path "multisig::ConfirmationStatus".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_multisig_ConfirmationStatus.

(* StructRecord
  {
    name := "Transaction";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("callee", Ty.path "multisig::AccountId");
        ("selector",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ]);
        ("input",
          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]);
        ("transferred_value", Ty.path "u128");
        ("gas_limit", Ty.path "u64");
        ("allow_reentry", Ty.path "bool")
      ];
  } *)

Module Impl_core_default_Default_for_multisig_Transaction.
  Definition Self : Ty.t := Ty.path "multisig::Transaction".
  
  Parameter default : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_Transaction.

(*
Enum Error
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "TransactionFailed";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_clone_Clone_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Parameter clone : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_multisig_Error.

Module Impl_core_marker_Copy_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_multisig_Error.

Module Impl_core_marker_StructuralPartialEq_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_multisig_Error.

Module Impl_core_cmp_PartialEq_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Parameter eq : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_multisig_Error.

Module Impl_core_cmp_Eq_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Parameter assert_receiver_is_total_eq : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_multisig_Error.

(* StructRecord
  {
    name := "Transactions";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("transactions",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ]);
        ("next_id", Ty.path "u32")
      ];
  } *)

Module Impl_core_default_Default_for_multisig_Transactions.
  Definition Self : Ty.t := Ty.path "multisig::Transactions".
  
  Parameter default : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_Transactions.

(* StructRecord
  {
    name := "Confirmation";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("transaction", Ty.path "u32");
        ("from", Ty.path "multisig::AccountId");
        ("status", Ty.path "multisig::ConfirmationStatus")
      ];
  } *)

(* StructRecord
  {
    name := "Revocation";
    const_params := [];
    ty_params := [];
    fields := [ ("transaction", Ty.path "u32"); ("from", Ty.path "multisig::AccountId") ];
  } *)

(* StructRecord
  {
    name := "Submission";
    const_params := [];
    ty_params := [];
    fields := [ ("transaction", Ty.path "u32") ];
  } *)

(* StructRecord
  {
    name := "Cancellation";
    const_params := [];
    ty_params := [];
    fields := [ ("transaction", Ty.path "u32") ];
  } *)

(* StructRecord
  {
    name := "Execution";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("transaction", Ty.path "u32");
        ("result",
          Ty.apply
            (Ty.path "core::result::Result")
            []
            [
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                ];
              Ty.path "multisig::Error"
            ])
      ];
  } *)

(* StructRecord
  {
    name := "OwnerAddition";
    const_params := [];
    ty_params := [];
    fields := [ ("owner", Ty.path "multisig::AccountId") ];
  } *)

(* StructRecord
  {
    name := "OwnerRemoval";
    const_params := [];
    ty_params := [];
    fields := [ ("owner", Ty.path "multisig::AccountId") ];
  } *)

(* StructRecord
  {
    name := "RequirementChange";
    const_params := [];
    ty_params := [];
    fields := [ ("new_requirement", Ty.path "u32") ];
  } *)

(*
Enum Event
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Confirmation";
        item := StructTuple [ Ty.path "multisig::Confirmation" ];
        discriminant := None;
      };
      {
        name := "Revocation";
        item := StructTuple [ Ty.path "multisig::Revocation" ];
        discriminant := None;
      };
      {
        name := "Submission";
        item := StructTuple [ Ty.path "multisig::Submission" ];
        discriminant := None;
      };
      {
        name := "Cancellation";
        item := StructTuple [ Ty.path "multisig::Cancellation" ];
        discriminant := None;
      };
      {
        name := "Execution";
        item := StructTuple [ Ty.path "multisig::Execution" ];
        discriminant := None;
      };
      {
        name := "OwnerAddition";
        item := StructTuple [ Ty.path "multisig::OwnerAddition" ];
        discriminant := None;
      };
      {
        name := "OwnerRemoval";
        item := StructTuple [ Ty.path "multisig::OwnerRemoval" ];
        discriminant := None;
      };
      {
        name := "RequirementChange";
        item := StructTuple [ Ty.path "multisig::RequirementChange" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_multisig_Env.
  Definition Self : Ty.t := Ty.path "multisig::Env".
  
  Parameter caller : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_caller : M.IsAssociatedFunction Self "caller" caller.
  
  Parameter emit_event : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_emit_event : M.IsAssociatedFunction Self "emit_event" emit_event.
  
  Parameter transferred_value : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_transferred_value :
    M.IsAssociatedFunction Self "transferred_value" transferred_value.
  
  Parameter account_id : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_account_id : M.IsAssociatedFunction Self "account_id" account_id.
End Impl_multisig_Env.

(* StructRecord
  {
    name := "Multisig";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("confirmations",
          Ty.apply
            (Ty.path "multisig::Mapping")
            []
            [ Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ]; Ty.tuple [] ]);
        ("confirmation_count",
          Ty.apply (Ty.path "multisig::Mapping") [] [ Ty.path "u32"; Ty.path "u32" ]);
        ("transactions",
          Ty.apply
            (Ty.path "multisig::Mapping")
            []
            [ Ty.path "u32"; Ty.path "multisig::Transaction" ]);
        ("transaction_list", Ty.path "multisig::Transactions");
        ("owners",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ]);
        ("is_owner",
          Ty.apply (Ty.path "multisig::Mapping") [] [ Ty.path "multisig::AccountId"; Ty.tuple [] ]);
        ("requirement", Ty.path "u32")
      ];
  } *)

Module Impl_core_default_Default_for_multisig_Multisig.
  Definition Self : Ty.t := Ty.path "multisig::Multisig".
  
  Parameter default : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_Multisig.

Parameter ensure_requirement_is_valid : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_ensure_requirement_is_valid :
  M.IsFunction "multisig::ensure_requirement_is_valid" ensure_requirement_is_valid.

Module Impl_multisig_Multisig.
  Definition Self : Ty.t := Ty.path "multisig::Multisig".
  
  Parameter init_env : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
  
  Parameter env : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  Parameter new : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  Parameter ensure_confirmed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_ensure_confirmed :
    M.IsAssociatedFunction Self "ensure_confirmed" ensure_confirmed.
  
  Parameter ensure_transaction_exists : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_ensure_transaction_exists :
    M.IsAssociatedFunction Self "ensure_transaction_exists" ensure_transaction_exists.
  
  Parameter ensure_owner : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_ensure_owner : M.IsAssociatedFunction Self "ensure_owner" ensure_owner.
  
  Parameter ensure_caller_is_owner : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_ensure_caller_is_owner :
    M.IsAssociatedFunction Self "ensure_caller_is_owner" ensure_caller_is_owner.
  
  Parameter ensure_from_wallet : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_ensure_from_wallet :
    M.IsAssociatedFunction Self "ensure_from_wallet" ensure_from_wallet.
  
  Parameter ensure_no_owner : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_ensure_no_owner :
    M.IsAssociatedFunction Self "ensure_no_owner" ensure_no_owner.
  
  Parameter add_owner : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_add_owner : M.IsAssociatedFunction Self "add_owner" add_owner.
  
  Parameter owner_index : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_owner_index : M.IsAssociatedFunction Self "owner_index" owner_index.
  
  Parameter clean_owner_confirmations : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_clean_owner_confirmations :
    M.IsAssociatedFunction Self "clean_owner_confirmations" clean_owner_confirmations.
  
  Parameter remove_owner : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_remove_owner : M.IsAssociatedFunction Self "remove_owner" remove_owner.
  
  Parameter replace_owner : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_replace_owner :
    M.IsAssociatedFunction Self "replace_owner" replace_owner.
  
  Parameter change_requirement : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_change_requirement :
    M.IsAssociatedFunction Self "change_requirement" change_requirement.
  
  Parameter confirm_by_caller : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_confirm_by_caller :
    M.IsAssociatedFunction Self "confirm_by_caller" confirm_by_caller.
  
  Parameter submit_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_submit_transaction :
    M.IsAssociatedFunction Self "submit_transaction" submit_transaction.
  
  Parameter take_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_take_transaction :
    M.IsAssociatedFunction Self "take_transaction" take_transaction.
  
  Parameter cancel_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_cancel_transaction :
    M.IsAssociatedFunction Self "cancel_transaction" cancel_transaction.
  
  Parameter confirm_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_confirm_transaction :
    M.IsAssociatedFunction Self "confirm_transaction" confirm_transaction.
  
  Parameter revoke_confirmation : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_revoke_confirmation :
    M.IsAssociatedFunction Self "revoke_confirmation" revoke_confirmation.
  
  Parameter invoke_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_invoke_transaction :
    M.IsAssociatedFunction Self "invoke_transaction" invoke_transaction.
  
  Parameter eval_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_eval_transaction :
    M.IsAssociatedFunction Self "eval_transaction" eval_transaction.
End Impl_multisig_Multisig.
