Library EVMOpSem.Lem.lem_function

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.


Require Import lem_bool.
Require Export lem_bool.
Require Import lem_basic_classes.
Require Export lem_basic_classes.

Require Import Program.Basics.
Require Export Program.Basics.






Definition rev_apply {a b : Type} (x : a) (f : a -> b) : b:= f x.


Definition curry {a b c : Type} (f : (a*b) % type -> c) : a -> b -> c:= (fun (a1 : a) (b1 : b) => f (a1, b1)).

Definition uncurry {a b c : Type} (f : a -> b -> c) (p : (a*b) % type) : c:=
  match ( (f,p)) with ( f, (a1, b1)) => f a1 b1 end.