diff --git a/execution/examples/EIP20Token.v b/execution/examples/EIP20Token.v
index 86909972..608b1e76 100644
--- a/execution/examples/EIP20Token.v
+++ b/execution/examples/EIP20Token.v
@@ -22,7 +22,6 @@ Import RecordSetNotations.
 
 Section EIP20Token.
   Context {BaseTypes : ChainBase}.
-  Set Primitive Projections.
   Set Nonrecursive Elimination Schemes.
 
   Definition TokenValue := N.
diff --git a/extraction/_CoqProject b/extraction/_CoqProject
index e964cc99..bec6c4fb 100644
--- a/extraction/_CoqProject
+++ b/extraction/_CoqProject
@@ -14,6 +14,7 @@ theories/Annotations.v
 theories/CameLIGOExtract.v
 theories/CameLIGOPretty.v
 theories/Certifying.v
+theories/CertifyingBeta.v
 theories/CertifyingEta.v
 theories/CertifyingInlining.v
 theories/ClosedAux.v
diff --git a/extraction/examples/CameLIGOExtractionTests.v b/extraction/examples/CameLIGOExtractionTests.v
index 2a244cca..5562dea0 100644
--- a/extraction/examples/CameLIGOExtractionTests.v
+++ b/extraction/examples/CameLIGOExtractionTests.v
@@ -344,14 +344,17 @@ Section CrowdfundingExtraction.
 End CrowdfundingExtraction.
 
 Section EIP20TokenExtraction.
+
   Import EIP20Token.
   Import RecordSetNotations.
 
+  Open Scope Z_scope.
+
   Definition init (ctx : ContractCallContext) (setup : EIP20Token.Setup) : option EIP20Token.State :=
     Some {| total_supply := setup.(init_amount);
-            balances := FMap.add (EIP20Token.owner setup) (init_amount setup) FMap.empty;
-            allowances := FMap.empty |}.
-  Open Scope Z_scope.
+            balances := Common.AddressMap.add (EIP20Token.owner setup) (init_amount setup) Common.AddressMap.empty;
+            allowances := Common.AddressMap.empty |}.
+
   Definition receive_ (chain : Chain)
        (ctx : ContractCallContext)
        (state : EIP20Token.State)
@@ -363,50 +366,24 @@ Section EIP20TokenExtraction.
     end.
   Close Scope Z_scope.
 
-  (* A specialized version of FMap's partial alter, w.r.t. FMap Address N *)
-  Definition partial_alter_addr_nat : string :=
-       "let partial_alter_addr_nat (f : nat option -> nat option)" ++ nl
-    ++ "                           (k : address)" ++ nl
-    ++ "                           (m : (address,nat) map) : (address,nat) map =" ++ nl
-    ++ "  match Map.find_opt k m with" ++ nl
-    ++ "    Some v -> Map.update k (f v) m" ++ nl
-    ++ "  | None -> Map.update k (f (None : nat option)) m" ++ nl.
-
-  Definition option_map_state_acts : string :=
-       "let option_map_state_acts (f : state -> (state * operation list)) (o : state option) =" ++ nl
-    ++ "  match o with" ++ nl
-    ++ "    Some a -> Some (f a)" ++ nl
-    ++ "    | None -> (None : (state * operation list))".
-
-  Definition bind_option_state : string :=
-       "let bind_option_state (a, b, c : unit) (m : state option) (f : state -> state option) : state option =" ++ nl
-    ++ "match m with" ++ nl
-    ++ "    Some a -> f a" ++ nl
-    ++ "  | None -> (None : state option)".
-
-  Definition with_default_N : string :=
-       "let with_default_N (n : nat) (m : nat option) : n =" ++ nl
-    ++ "  match m with" ++ nl
-    ++ "    Some m -> m" ++ nl
-    ++ "  | None -> n".
-
   Definition LIGO_EIP20Token_MODULE : CameLIGOMod EIP20Token.Msg ContractCallContext EIP20Token.Setup EIP20Token.State ActionBody :=
   {| (* a name for the definition with the extracted code *)
       lmd_module_name := "cameLIGO_eip20token" ;
 
       (* definitions of operations on pairs and ints *)
-      lmd_prelude := CameLIGOPrelude;
+      lmd_prelude := CameLIGOPrelude ++ nl ++
+                     dummy_chain;
 
       (* initial storage *)
       lmd_init := init ;
 
+      (* NOTE: printed as local [let]-bound definitions in the init *)
       lmd_init_prelude := "";
 
+      (* TODO: maybe not needed, [lmd_prelude] should be enough *)
+      lmd_receive_prelude := "";
+
       (* the main functionality *)
-      lmd_receive_prelude := partial_alter_addr_nat ++ nl ++
-      option_map_state_acts ++ nl ++
-      bind_option_state ++ nl ++
-      with_default_N;
       lmd_receive := receive_ ;
 
       (* code for the entry point *)
@@ -414,38 +391,47 @@ Section EIP20TokenExtraction.
                         ++ CameLIGOPretty.printMain |}.
 
   Definition TT_remap_eip20token : list (kername * string) :=
-  [
-    remap <%% @ContractCallContext %%> "(adress * (address * int))"
-  ; remap <%% eqb_addr %%> "eq_addr"
-  ; remap <%% @Extras.with_default %%> "with_default_N"
-  ; remap <%% @Monads.bind %%> "bind_option_state"
-  ; remap <%% Monads.Monad_option %%> "()"
-
-  ; remap <%% @stdpp.base.insert %%> "Map.add"
-  ; remap <%% @stdpp.base.lookup %%> "Map.find_opt"
-  ; remap <%% @stdpp.base.empty %%> "Map.empty"
-  ; remap <%% @stdpp.base.partial_alter %%> "partial_alter_addr_nat"
-  ; remap <%% @gmap.gmap_partial_alter %%> ""
-  ; remap <%% @fin_maps.map_insert %%> ""
-  ; remap <%% @gmap.gmap_empty %%> ""
-  ; remap <%% @gmap.gmap_lookup %%> ""
-  ; remap <%% @address_eqdec %%> ""
-  ; remap <%% @address_countable %%> ""
-  ; remap <%% option_map %%> "option_map_state_acts"
+    TT_remap_default ++ [
+    (* TODO: is it of a correct type? *)
+    remap <%% @ContractCallContext %%> "(address * (address * int))"
+  ; remap <%% @ctx_from %%> "fst" (* small hack, but valid since ContractCallContext is mapped to a tuple *)
+
+  ; remap <%% @ActionBody %%> "operation"
+
+  ; remap <%% @FMap %%> "map"
+  ; remap <%% @Common.AddressMap.add %%> "Map.add"
+  ; remap <%% @Common.AddressMap.find %%> "Map.find_opt"
+  ; remap <%% @Common.AddressMap.empty %%> "Map.empty"
   ].
 
+  Definition TT_inlines_eip20token : list kername :=
+    [
+      <%% Monads.Monad_option %%>
+    ; <%% @Monads.bind %%>
+    ; <%% @Monads.ret %%>
+    ; <%% bool_rect %%>
+    ; <%% bool_rec %%>
+    ; <%% option_map %%>
+    ; <%% @Extras.with_default %%>
+
+    ; <%% @setter_from_getter_State_balances %%>
+    ; <%% @setter_from_getter_State_total_supply %%>
+    ; <%% @setter_from_getter_State_allowances %%>
+    ; <%% @set_State_balances %%>
+    ; <%% @set_State_allowances%%>
+    ; <%% @Common.AddressMap.AddrMap %%>
+    ].
+
+
   Definition TT_rename_eip20token :=
     [ ("Z0" ,"0tez")
-    ; ("N0", "0n")
-    ; ("N1", "1n")
+    ; ("N0", "0")
+    ; ("N1", "1")
     ; ("nil", "[]")
-      (* monad hack *)
-    ; ("Monad_option", "()")
     ; ("tt", "()") ].
 
   Time MetaCoq Run
-  (CameLIGO_prepare_extraction PREFIX [] TT_remap_eip20token TT_rename_eip20token LIGO_EIP20Token_MODULE).
-
+  (CameLIGO_prepare_extraction PREFIX TT_inlines_eip20token TT_remap_eip20token TT_rename_eip20token LIGO_EIP20Token_MODULE).
 
   Time Definition cameLIGO_eip20token := Eval vm_compute in cameLIGO_eip20token_prepared.
 
@@ -461,6 +447,35 @@ Section TestExtractionPlayground.
   Import RecordSetNotations.
 
   Open Scope N_scope.
+
+  (* A specialized version of FMap's partial alter, w.r.t. FMap Address N *)
+  Definition partial_alter_addr_nat : string :=
+       "let partial_alter_addr_nat (f : nat option -> nat option)" ++ nl
+    ++ "                           (k : address)" ++ nl
+    ++ "                           (m : (address,nat) map) : (address,nat) map =" ++ nl
+    ++ "  match Map.find_opt k m with" ++ nl
+    ++ "    Some v -> Map.update k (f v) m" ++ nl
+    ++ "  | None -> Map.update k (f (None : nat option)) m" ++ nl.
+
+  Definition option_map_state_acts : string :=
+       "let option_map_state_acts (f : state -> (state * operation list)) (o : state option) =" ++ nl
+    ++ "  match o with" ++ nl
+    ++ "    Some a -> Some (f a)" ++ nl
+    ++ "    | None -> (None : (state * operation list))".
+
+  Definition bind_option_state : string :=
+       "let bind_option_state (a, b, c : unit) (m : state option) (f : state -> state option) : state option =" ++ nl
+    ++ "match m with" ++ nl
+    ++ "    Some a -> f a" ++ nl
+    ++ "  | None -> (None : state option)".
+
+  Definition with_default_N : string :=
+       "let with_default_N (n : nat) (m : nat option) : n =" ++ nl
+    ++ "  match m with" ++ nl
+    ++ "    Some m -> m" ++ nl
+++ "  | None -> n".
+
+
   Definition test_try_transfer (from : Address)
        (to : Address)
        (amount : TokenValue)
diff --git a/extraction/examples/ERC20LiquidityExtraction.v b/extraction/examples/ERC20LiquidityExtraction.v
index 3c2a8b6d..ae743999 100644
--- a/extraction/examples/ERC20LiquidityExtraction.v
+++ b/extraction/examples/ERC20LiquidityExtraction.v
@@ -98,10 +98,10 @@ Section EIP20TokenExtraction.
     match maybe_msg with
     | Some (transfer to_addr amountt) => without_actions (try_transfer sender to_addr amountt state)
     | Some (transfer_from from to_addr amountt) => without_actions (try_transfer_from sender from to_addr amountt state)
-    (* 'approve' endpoint not included in this test *)
+   | Some (approve delegate amount) => without_actions (try_approve sender delegate amount state)
     | _ => None
     end.
-  
+
   Definition receive_wrapper
              (params : params)
              (st : State) : option (list ActionBody × State) :=
@@ -139,9 +139,11 @@ Section EIP20TokenExtraction.
 
   
   Definition TT_remap_eip20token : list (kername * string) :=
-  TT_remap_default ++ [
+    TT_remap_default ++ [
+    (* FIXME: it seems like the context type is wrong *)
     remap <%% @ContractCallContext %%> "(address * (address * int))"
   ; remap <%% @ctx_from %%> "fst" (* small hack, but valid since ContractCallContext is mapped to a tuple *)
+  ; remap <%% gmap.gmap %%> "map"
   ; remap <%% @AddressMap.add %%> "Map.add"
   ; remap <%% @AddressMap.find %%> "Map.find"
   ; remap <%% @AddressMap.empty %%> "(Map [])"
@@ -169,6 +171,8 @@ Section EIP20TokenExtraction.
     ; <%% @setter_from_getter_State_allowances %%>
     ; <%% @set_State_balances %%>
     ; <%% @set_State_allowances%%>
+
+    ; <%% @Common.AddressMap.AddrMap %%>
     ].
   
   Time MetaCoq Run
@@ -176,7 +180,7 @@ Section EIP20TokenExtraction.
       tmDefinition EIP20Token_MODULE.(lmd_module_name) t).
 
   Print liquidity_eip20token.
-
+  
   (** We redirect the extraction result for later processing and compiling with the Liquidity compiler *)
   Redirect "./examples/liquidity-extract/liquidity_eip20token.liq" Compute liquidity_eip20token.
 
diff --git a/extraction/examples/ElmExtractTests.v b/extraction/examples/ElmExtractTests.v
index 03bb608c..2e86f975 100644
--- a/extraction/examples/ElmExtractTests.v
+++ b/extraction/examples/ElmExtractTests.v
@@ -12,6 +12,7 @@ From Coq Require Import String.
 From MetaCoq.Template Require Import Ast.
 From MetaCoq.Template Require Import Kernames.
 From MetaCoq.Template Require Import Loader.
+From MetaCoq.Template Require Import TemplateMonad.
 From MetaCoq Require Import monad_utils.
 From MetaCoq Require Import utils.
 
@@ -370,3 +371,133 @@ Module ex_infix1.
 "  in";
 "  map2" $>. reflexivity. Qed.
 End ex_infix1.
+
+Module recursor_ex.
+
+  Program Definition test {A B : Type} (f : A -> B) (xs : list A) : list B :=
+    list_rect (fun x => list B) [] (fun x _ rec => f x :: rec) xs.
+
+  Lemma test_is_map : @test = @map.
+  Proof. reflexivity. Qed.
+
+  Print test.
+
+  MetaCoq Quote Recursively Definition ex := @test.
+
+  Compute general_extract ex [] [].
+End recursor_ex.
+
+Module type_scheme_ex.
+
+  Definition general_extract_tc (p : program) (ignore: list kername) (TT : list (kername * string)) : TemplateMonad string :=
+  entry <- match p.2 with
+           | tConst kn _ => ret kn
+           | tInd ind _ => ret (inductive_mind ind)
+           | _ => tmFail "Expected program to be a tConst or tInd"
+           end;;
+  res <- tmEval lazy (extract_template_env
+                       no_check_args
+                       p.1
+                       (KernameSet.singleton entry)
+                       (fun k => existsb (eq_kername k) ignore));;
+  match res with
+  | Ok Σ =>
+    tmPrint Σ;;
+    let TT_fun kn := option_map snd (List.find (fun '(kn',v) => eq_kername kn kn') TT) in
+    s <- tmEval lazy (finish_print (print_env Σ TT_fun));;
+    match s with
+    | Ok (_,s) => ret s
+    | Err s => tmFail s
+    end
+  | Err s => tmFail s
+  end.
+
+
+  (* A simple type abbreviation *)
+
+  Definition Arrow (A B : Type) := A -> B.
+
+  MetaCoq Quote Recursively Definition Arrow_syn := Arrow.
+
+  Example Arrow_test :
+    general_extract Arrow_syn [] [] = Ok "type alias Arrow a b = a -> b".
+  Proof. vm_compute. reflexivity. Qed.
+
+  Definition Triple (A B C : Type) := A * B * C.
+
+  MetaCoq Quote Recursively Definition Triple_syn := Triple.
+
+  MetaCoq Run (general_extract_tc Triple_syn [] []).
+
+  Example Triple_test :
+    general_extract Triple_syn [] [] = Ok <$
+"type Prod a b";
+"  = Pair a b";
+"";
+"type alias Triple a b c = Prod (Prod a b) c" $>.
+  Proof. vm_compute. reflexivity. Qed.
+
+  Module LetouzeyExample.
+  (* An example from Letouzey's thesis, Section 3.3.4 *)
+
+  Definition P (b : bool) : Set := if b then nat else bool.
+  Definition Sch3 : (bool -> Set) -> Set := fun X => X true -> X false.
+  Definition Sch3_applied := (fun X => X true -> X false) (fun b => if b then nat else bool).
+
+  MetaCoq Quote Recursively Definition Sch3_syn := Sch3.
+
+  Example Sch3_test :
+    general_extract Sch3_syn [] [] = Ok "type alias Sch3 x = x -> x".
+  Proof. vm_compute. reflexivity. Qed.
+
+  MetaCoq Quote Recursively Definition Sch3_applied_syn := Sch3_applied.
+
+  (* In this case, the application reduces to a type with no type parameters *)
+  Example Sch3_applied_test :
+    general_extract Sch3_applied_syn [] [] = Ok <$
+"type Bool";
+"  = True";
+"  | False";
+"";
+"type Nat";
+"  = O";
+"  | S Nat";
+"";
+"type alias Sch3_applied = Nat -> Bool" $>.
+  Proof. vm_compute. reflexivity. Qed.
+
+  End LetouzeyExample.
+
+
+  (* [Vec] is a common example of using a type scheme to abbreviate a type *)
+
+  Definition vec (A : Type) (n : nat) := {xs : list A | length xs = n}.
+
+  Program Definition singleton_vec (n : nat) : vec nat 1 := [n].
+  Next Obligation. easy. Qed.
+
+  MetaCoq Quote Recursively Definition singleton_vec_syn := singleton_vec.
+
+  MetaCoq Run (general_extract_tc singleton_vec_syn [] []).
+
+  Example singleton_vec_test:
+    general_extract singleton_vec_syn [] [] = Ok <$
+"type Nat";
+"  = O";
+"  | S Nat";
+"";
+"type Sig a";
+"  = Exist a";
+"";
+"type List a";
+"  = Nil";
+"  | Cons a (List a)";
+"";
+"type alias Vec a = Sig (List a)";
+"";
+"singleton_vec : Nat -> Vec Nat";
+"singleton_vec n =";
+"  Exist (Cons n Nil)" $>.
+  Proof. vm_compute. reflexivity. Qed.
+
+End type_scheme_ex.
diff --git a/extraction/theories/CameLIGOExtract.v b/extraction/theories/CameLIGOExtract.v
index 752d316e..692f5802 100644
--- a/extraction/theories/CameLIGOExtract.v
+++ b/extraction/theories/CameLIGOExtract.v
@@ -14,7 +14,7 @@ From MetaCoq.Template Require Pretty.
 From ConCert.Extraction Require Import ResultMonad.
 From ConCert.Extraction Require Import CertifyingInlining.
 From ConCert.Utils Require Import RecordSet RecordUpdate StringExtra.
-From ConCert.Execution Require Import Blockchain Serializable.
+From ConCert.Execution Require Import Blockchain Serializable Common.
 
 From ConCert.Extraction Require Import CameLIGOPretty
      Common ExAst Erasure Optimize Extraction TypeAnnotations Annotations Utils SpecializeChainBase.
@@ -42,15 +42,25 @@ Arguments lmd_receive {_ _ _ _ _ _}.
 Arguments lmd_receive_prelude {_ _ _ _ _ _}.
 Arguments lmd_entry_point {_ _ _ _ _ _}.
 
+(* We override masks for *some* constants that have only logical parameters, like
+   [@AddressMap.empty]. Our optimisation conservatively keeps one parameter
+   if all the parameters are logical. This is necessary because such definitions
+   might use something like [false_rect] and removing all the arguments will force evaluating their bodies, which can lead to an exception or looping depending
+   on how the elimination from the empty types is implemented.
+   However, for [AddressMap.empty] is completely safe to remove all arguments, since it's an abbreviation for a constructor.*)
+Definition overridden_masks (kn : kername) : option bitmask :=
+  if eq_kername kn <%% @AddressMap.empty %%> then Some [true]
+  else None.
+
 Definition cameligo_args :=
        {| optimize_prop_discr := true;
-               extract_transforms := [Optimize.dearg_transform
-                              (fun _ => None)
-                              true
-                              false (* cannot have partially applied ctors *)
-                              true
-                              true
-                              true] |}.
+          extract_transforms := [Optimize.dearg_transform
+                                   overridden_masks
+                                   true
+                                   false (* cannot have partially applied ctors *)
+                                   true
+                                   true
+                                   true] |}.
 
 Import PCUICAst PCUICTyping.
 Definition annot_extract_env_cameligo
@@ -103,7 +113,8 @@ Definition TT_remap_default : list (kername * string) :=
   [
     (* types *)
     remap <%% Z %%> "tez"
-  ; remap <%% N %%> "nat"
+  (* NOTE: subtracting two [nat]s gives [int], so we remap [N] to [int] *)
+  ; remap <%% N %%> "int"
   ; remap <%% nat %%> "nat"
   ; remap <%% bool %%> "bool"
   ; remap <%% unit %%> "unit"
@@ -219,7 +230,7 @@ Definition printCameLIGODefs `{ChainBase} {Base : ChainBase} {msg ctx params sto
           (* map snd (filter (negb ∘ (eq_kername init) ∘ fst) ldef_list) in *)
         let res : string :=
             String.concat (nl ++ nl) (defs ++ (cons init_code nil)) in
-        (wrap_in_delimiters (String.concat (nl ++ nl) [prelude; res; entry_point])) |> inl
+        (wrap_in_delimiters (String.concat (nl ++ nl) [res; entry_point])) |> inl
       | None => inr "Error: Empty body for init"
       end
     | Some _ => inr "Error: init must be a constant"
diff --git a/extraction/theories/CertifyingBeta.v b/extraction/theories/CertifyingBeta.v
new file mode 100644
index 00000000..9b0171e4
--- /dev/null
+++ b/extraction/theories/CertifyingBeta.v
@@ -0,0 +1,92 @@
+From Coq Require Import List String Bool Basics.
+
+From ConCert.Extraction Require Import Transform.
+From ConCert.Extraction Require Import Optimize.
+From ConCert.Extraction Require Import Common.
+From ConCert.Extraction Require Import ResultMonad.
+From ConCert.Extraction Require Import Utils.
+From ConCert.Extraction Require Import Certifying.
+
+From MetaCoq.Template Require Import All Kernames.
+
+Import ListNotations.
+Import MonadNotation.
+
+Section betared.
+  Context (Σ : global_env).
+
+  Fixpoint decompose_lam (t : term) {struct t} :
+  (list aname × list term) × term :=
+    match t with
+    | tLambda na A B =>
+      let (nAs, B0) := decompose_lam B in
+      let (ns, As) := nAs in (na :: ns, A :: As, B0)
+    | _ => ([], [], t)
+    end.
+
+  Fixpoint betared_aux (args : list term) (t : term) : term :=
+      match t with
+      | tApp hd args0 => betared_aux (map (betared_aux []) args0 ++ args) hd
+      | tCast t0 _ _ => betared_aux args t0
+      | tLambda na ty body =>
+        let b := betared_aux [] body in
+        beta_body (tLambda na ty b) args
+      | t => mkApps (map_subterms (betared_aux []) t) args
+      end.
+
+  Definition betared : term -> term := betared_aux [].
+
+  Definition betared_in_constant_body cst :=
+    {| cst_type := cst_type cst;
+       cst_universes := cst_universes cst;
+       cst_body := option_map betared (cst_body cst) |}.
+
+  Definition betared_in_decl d :=
+    match d with
+    | ConstantDecl cst => ConstantDecl (betared_in_constant_body cst)
+    | _ => d
+    end.
+
+End betared.
+
+Definition betared_in_env (Σ : global_env) : global_env :=
+  fold_right (fun '(kn, decl) Σ => (kn, betared_in_decl decl) :: Σ) [] Σ.
+
+Definition betared_global_env_template
+           (mpath : modpath)
+           (Σ : global_env)
+           (seeds : KernameSet.t)
+  : TemplateMonad global_env :=
+  let suffix := "_after_betared" in
+  Σinlined <- tmEval lazy (betared_in_env Σ);;
+  gen_defs_and_proofs Σ Σinlined mpath suffix seeds;;
+  ret Σinlined.
+
+(* Mainly for testing purposes *)
+Definition betared_def {A}
+           (def : A) : TemplateMonad _ :=
+  mpath <- tmCurrentModPath tt;;
+  p <- tmQuoteRecTransp def false ;;
+  kn <- Common.extract_def_name def ;;
+  betared_global_env_template mpath p.1 (KernameSet.singleton kn).
+
+
+Definition template_betared : TemplateTransform :=
+  fun Σ => Ok (timed "Inlining" (fun _ => betared_in_env Σ)).
+
+Module Ex1.
+
+  Definition foo (n : nat) := (fun x => x) n.
+
+  MetaCoq Run (betared_def foo).
+
+  MetaCoq Quote Recursively Definition foo_after :=
+    ConCert_Extraction_CertifyingBeta_Ex1_foo_after_betared.
+
+  MetaCoq Quote Recursively Definition foo_before := foo.
+
+  Lemma after_not_before :
+    lookup_env foo_after.1 <%% ConCert_Extraction_CertifyingBeta_Ex1_foo_after_betared %%> =
+    lookup_env foo_before.1 <%% foo %%> -> False.
+  Proof. easy. Qed.
+End Ex1.
diff --git a/extraction/theories/CertifyingEta.v b/extraction/theories/CertifyingEta.v
index f89229a5..272220e3 100644
--- a/extraction/theories/CertifyingEta.v
+++ b/extraction/theories/CertifyingEta.v
@@ -420,8 +420,8 @@ Module Examples.
     MetaCoq Quote Recursively Definition match_ex1__ := match_ex1.
     MetaCoq Run (eta_expand_def
                    (fun _ => None)
-     (* We set the trimmig of masks to true, so the procedure does't not perform full expansion.
-        That way we can test the expansion of branches *)
+    (* We set the trimming of masks to true, so the procedure does't perform full expansion.
+       That way we can test the expansion of branches *)
                    true true
                    match_ex1).
 
diff --git a/extraction/theories/CertifyingInlining.v b/extraction/theories/CertifyingInlining.v
index ac355ad6..ad8765e8 100644
--- a/extraction/theories/CertifyingInlining.v
+++ b/extraction/theories/CertifyingInlining.v
@@ -8,6 +8,7 @@ From Coq Require Import List String Bool Basics.
 From ConCert.Extraction Require Import Transform.
 From ConCert.Extraction Require Import Optimize.
 From ConCert.Extraction Require Import Common.
+From ConCert.Extraction Require Import CertifyingBeta.
 From ConCert.Extraction Require Import ResultMonad.
 From ConCert.Extraction Require Import Utils.
 From ConCert.Extraction Require Import Certifying.
@@ -21,31 +22,6 @@ Section inlining.
   Context (should_inline : kername -> bool).
   Context (Σ : global_env).
 
-  Fixpoint beta_body (body : term) (args : list term) {struct args} : term :=
-    match args with
-    | [] => body
-    | a :: args =>
-      match body with
-      | tLambda na _ body => beta_body (body{0 := a}) args
-      | _ => mkApps body (a :: args)
-      end
-    end.
-
-  Definition iota_body (body : term) : term :=
-    match body with
-    | tCase (ind, pars, _) _ discr brs =>
-      let (hd, args) := decompose_app discr in
-      match hd with
-      | tConstruct _ c _ =>
-        match nth_error brs c with
-        | Some (_, br) => beta_body br (skipn pars args)
-        | None => body
-        end
-      | _ => body
-      end
-    | t => t
-    end.
-
   Definition inline_const (kn : kername) (u : Instance.t) (args : list term) : term :=
     let const := tConst kn u in
     match lookup_env Σ kn with
@@ -54,29 +30,13 @@ Section inlining.
       | Some body (* once told me *) =>
         (* Often the first beta will expose an iota (record projection),
                and the projected field is often a function, so we do another beta *)
-              let (hd, args) := decompose_app (beta_body body args) in
-              beta_body (iota_body hd) args
+        let (hd, args) := decompose_app (beta_body body args) in
+        beta_body (iota_body hd) args
       | None => tApp const args
       end
     | _ => tApp const args
     end.
 
-  Definition map_subterms (f : term -> term) (t : term) : term :=
-  match t with
-  | tEvar n ts => tEvar n (map f ts)
-  | tCast t kind ty => tCast (f t) kind (f ty)
-  | tProd na ty body => tProd na (f ty) (f body)
-  | tLambda na ty body => tLambda na (f ty) (f body)
-  | tLetIn na val ty body => tLetIn na (f val) (f ty) (f body)
-  | tApp hd arg => tApp (f hd) (map f arg)
-  | tCase p ty disc brs =>
-    tCase p (f ty) (f disc) (map (on_snd f) brs)
-  | tProj p t => tProj p (f t)
-  | tFix def i => tFix (map (map_def f f) def) i
-  | tCoFix def i => tCoFix (map (map_def f f) def) i
-  | t => t
-  end.
-
   Fixpoint inline_aux (args : list term) (t : term) : term :=
     match t with
     | tApp hd args0 => inline_aux (map (inline_aux []) args0 ++ args) hd
@@ -93,10 +53,15 @@ Section inlining.
         | Some (ConstantDecl cst) =>
           match cst_body cst with
           | Some body (* once told me *) =>
-            (* NOTE: Often the first beta will expose an iota (record projection),
-               and the projected field is often a function, so we do another beta *)
             let (hd, args) := decompose_app (beta_body body args) in
-            beta_body (iota_body hd) args
+          (* NOTE: Often the first beta will expose an iota (record projection),
+             and the projected field is often a function, so we do another beta *)
+            let res := beta_body (iota_body hd) args in
+          (* NOTE: after we beta-reduced the function coming from projection,
+             it might intorduce new redexes. This is often the case when using
+             option monads. Therefore, we do a pass that find the redexes and
+             beta-reduces them further. *)
+            betared res
           | None => mkApps (tConst kn u) args
           end
         | _ => mkApps (tConst kn u) args
@@ -109,14 +74,34 @@ Section inlining.
   Definition inline : term -> term := inline_aux [].
 
   Definition inline_in_constant_body cst :=
-    {| cst_type := cst_type cst;
+    {| cst_type := inline (cst_type cst);
        cst_universes := cst_universes cst;
        cst_body := option_map inline (cst_body cst) |}.
 
+  Definition inline_oib (oib : one_inductive_body) :=
+    {| ind_name := oib.(ind_name);
+       ind_type := inline oib.(ind_type);
+       ind_kelim := oib.(ind_kelim);
+       ind_ctors := map (fun '(c_nm,c_ty,i) => (c_nm, inline c_ty,i)) oib.(ind_ctors);
+       ind_projs := map (fun '(p_nm, p_ty) => (p_nm, inline p_ty)) oib.(ind_projs);
+       ind_relevance := oib.(ind_relevance) |}.
+
+  Definition inline_context_decl (cd : context_decl) : context_decl :=
+    {| decl_name := cd.(decl_name);
+       decl_body := option_map inline cd.(decl_body);
+       decl_type := cd.(decl_type) |}.
+
   Definition inline_in_decl d :=
     match d with
     | ConstantDecl cst => ConstantDecl (inline_in_constant_body cst)
-    | _ => d
+    | InductiveDecl mib =>
+      InductiveDecl
+        {| ind_finite := mib.(ind_finite);
+           ind_npars := mib.(ind_npars);
+           ind_params :=map inline_context_decl mib.(ind_params);
+           ind_bodies := map inline_oib mib.(ind_bodies);
+           ind_universes := mib.(ind_universes);
+           ind_variance := mib.(ind_variance) |}
     end.
 
 End inlining.
@@ -206,4 +191,18 @@ Module Tests.
     Definition bar : nat -> nat := fun x => ((foo (x * 2)) : nat -> nat) x.
     MetaCoq Run (inline_def (fun kn => eq_kername <%% foo %%> kn) bar).
   End Ex5.
+
+  (* Inlining type aliases in inductives *)
+  Module Ex6.
+
+    Definition my_prod (A B : Type) : Type := A * B.
+
+    Inductive blah :=
+    | blah_ctor : my_prod nat bool -> blah.
+
+    Definition foo (p : my_prod nat bool) : blah := blah_ctor p.
+
+    MetaCoq Run (inline_def (fun kn => eq_kername <%% my_prod %%> kn) foo).
+  End Ex6.
+
 End Tests.
diff --git a/extraction/theories/Common.v b/extraction/theories/Common.v
index f095c2af..62b93858 100644
--- a/extraction/theories/Common.v
+++ b/extraction/theories/Common.v
@@ -1,5 +1,6 @@
 From ConCert.Extraction Require Import ResultMonad.
 From MetaCoq.Template Require Import Ast.
+From MetaCoq.Template Require Import LiftSubst.
 From MetaCoq.Template Require Import AstUtils.
 From MetaCoq.Template Require Import BasicAst.
 From MetaCoq.Template Require Import Loader.
@@ -141,3 +142,44 @@ Fixpoint update_global_env (Σ : global_env) (Σup : global_env) : global_env :=
                     end
   | [] => []
   end.
+
+Definition map_subterms (f : term -> term) (t : term) : term :=
+  match t with
+  | tEvar n ts => tEvar n (map f ts)
+  | tCast t kind ty => tCast (f t) kind (f ty)
+  | tProd na ty body => tProd na (f ty) (f body)
+  | tLambda na ty body => tLambda na (f ty) (f body)
+  | tLetIn na val ty body => tLetIn na (f val) (f ty) (f body)
+  | tApp hd arg => tApp (f hd) (map f arg)
+  | tCase p ty disc brs =>
+    tCase p (f ty) (f disc) (map (on_snd f) brs)
+  | tProj p t => tProj p (f t)
+  | tFix def i => tFix (map (map_def f f) def) i
+  | tCoFix def i => tCoFix (map (map_def f f) def) i
+  | t => t
+  end.
+
+Fixpoint beta_body (body : term) (args : list term) {struct args} : term :=
+  match args with
+  | [] => body
+  | a :: args =>
+    match body with
+    | tLambda na _ body => beta_body (body{0 := a}) args
+    | _ => mkApps body (a :: args)
+    end
+  end.
+
+Definition iota_body (body : term) : term :=
+  match body with
+  | tCase (ind, pars, _) _ discr brs =>
+    let (hd, args) := decompose_app discr in
+    match hd with
+    | tConstruct _ c _ =>
+      match nth_error brs c with
+      | Some (_, br) => beta_body br (skipn pars args)
+      | None => body
+      end
+    | _ => body
+    end
+  | t => t
+  end.
diff --git a/extraction/theories/LPretty.v b/extraction/theories/LPretty.v
index f71a52ab..bbf90c4e 100644
--- a/extraction/theories/LPretty.v
+++ b/extraction/theories/LPretty.v
@@ -87,13 +87,20 @@ Section print_term.
     | TApp t1 t2 => get_tapp_hd t1
     | _ => bt
     end.
+  
+  Definition print_type_var (v : name) (i : nat) :=
+    match v with
+    | nNamed nm => "'" ++ uncapitalize nm
+    | nAnon => "anon_tvar" ++ string_of_nat i
+    end.
 
-  Definition print_box_type (prefix : string) (TT : env string)
+  
+  Definition print_box_type (prefix : string) (TT : env string) (vars : list name)
     : box_type -> string :=
     fix go  (bt : box_type) :=
   match bt with
   | TBox => "unit"
-  | TArr dom codom => parens (negb (is_arr dom)) (go dom) ++ " → " ++ go codom
+  | TArr dom codom => parens (negb (is_arr dom)) (go dom) ++ " -> " ++ go codom
   | TApp t1 t2 =>
     let hd := get_tapp_hd t1 in
     let args := map_targs go bt in
@@ -105,7 +112,10 @@ Section print_term.
       else parens false (print_uncurried "" args ++ " " ++ go hd)
     | _ => parens false (print_uncurried "" args ++ " " ++ go hd)
     end
-  | TVar i => "'a" ++ string_of_nat i (* TODO: pass context with type variables *)
+  | TVar i => match nth_error vars i with
+             | Some nm => print_type_var nm i
+             | None => "UnknownTypeVar(" ++ string_of_nat i ++ ")"
+             end
   | TInd s =>
     let full_ind_name := string_of_kername s.(inductive_mind) in
     uncapitalize (from_option (look TT full_ind_name) (prefix ++ s.(inductive_mind).2))
@@ -119,45 +129,48 @@ Section print_term.
   Definition print_ctor
              (prefix : string)
              (TT : env string)
+             (vars : list name)
              (ctor : ident × list (name × box_type)) :=
     let (nm,tys) := ctor in
     let nm := capitalize nm in
     match tys with
     | [] => prefix ++ nm
     | _ => prefix ++ nm ++ " of "
-                  ++ concat " * " (map (print_box_type prefix TT ∘ snd) tys)
+                  ++ concat " * " (map (print_box_type prefix TT vars ∘ snd) tys)
     end.
   
-  Definition print_proj (prefix : string) (TT : env string) (proj : ident × box_type) : string :=
+  Definition print_proj (prefix : string)
+             (TT : env string)
+             (vars : list name)
+             (proj : ident × box_type) : string :=
     let (nm, ty) := proj in
     prefix
       ^ nm
       ^ " : "
-      ^ print_box_type prefix TT ty.
+      ^ print_box_type prefix TT vars ty.
 
   Definition print_inductive (prefix : string) (TT : env string)
              (oib : ExAst.one_inductive_body) :=
     let ind_nm := from_option (lookup TT oib.(ExAst.ind_name))
                               (prefix ++ oib.(ExAst.ind_name)) in
-    let print_type_var (i : nat) :=
-        "'a" ++ string_of_nat i in
+    let vars := map tvar_name oib.(ind_type_vars) in
     let params :=
         if (Nat.eqb #|oib.(ind_type_vars)| 0) then ""
-        else let ps := concat "," (mapi (fun i _ => print_type_var i) oib.(ind_type_vars)) in
-             (parens (Nat.eqb #|oib.(ind_type_vars)| 1) ps) ++ " " in
+        else let ps := concat "," (mapi (fun i v => print_type_var v i) vars) in
+             (parens (Nat.ltb #|oib.(ind_type_vars)| 1) ps) ++ " " in
     (* one-constructor inductives with non-empty ind_projs (projection identifiers) 
        are assumed to be records *)
     match oib.(ExAst.ind_ctors), oib.(ExAst.ind_projs) with
     | [build_record_ctor], _::_ =>
       let '(_, ctors) := build_record_ctor in
       let projs_and_ctors := combine oib.(ExAst.ind_projs) ctors in
-      let projs_and_ctors_printed := map (fun '(p, (proj_nm, ty)) => print_proj (capitalize prefix) TT (p.1, ty)) projs_and_ctors in
+      let projs_and_ctors_printed := map (fun '(p, (proj_nm, ty)) => print_proj (capitalize prefix) TT vars (p.1, ty)) projs_and_ctors in
       "type " ++ params ++ uncapitalize ind_nm ++ " = {" ++ nl
               ++ concat (";" ++ nl) projs_and_ctors_printed ++ nl
               ++  "}"
     | _,_ => "type " ++ params ++ uncapitalize ind_nm ++" = "
             ++ nl
-            ++ concat "| " (map (fun p => print_ctor (capitalize prefix) TT p ++ nl) oib.(ExAst.ind_ctors))
+            ++ concat "| " (map (fun p => print_ctor (capitalize prefix) TT vars p ++ nl) oib.(ExAst.ind_ctors))
     end.
 
   Definition is_sort (t : Ast.term) :=
@@ -528,11 +541,11 @@ Definition print_decl (prefix : string)
            (decl_name : string)
            (modifier : option string)
            (wrap : string -> string)
-           (ty : box_type)
+           (ty : list name × box_type)
            (t : term) :=
-  let (tys,_) := decompose_arr ty in
+  let (tys,_) := decompose_arr ty.2 in
   let (args,lam_body) := Edecompose_lam t in
-  let targs := combine args (map (print_box_type prefix TT) tys) in
+  let targs := combine args (map (print_box_type prefix TT ty.1) tys) in
   let printed_targs :=
       map (fun '(x,ty) => parens false (uncapitalize (string_of_name x) ++ " : " ++ ty)) targs in
   let decl := uncapitalize prefix ++ uncapitalize decl_name ++ " " ++ concat " " printed_targs in
@@ -555,7 +568,7 @@ Definition print_init (prefix : string)
   let ty := cst.(ExAst.cst_type) in
   let (tys,_) := decompose_arr ty.2 in
   let (args,lam_body) := Edecompose_lam b in
-  let targs_inner := combine args (map (print_box_type prefix TT) tys) in
+  let targs_inner := combine args (map (print_box_type prefix TT ty.1) tys) in
   let printed_targs_inner :=
       map (fun '(x,ty) => parens false (string_of_name x ++ " : " ++ ty)) targs_inner in
   let decl_inner := "inner " ++ concat " " printed_targs_inner in
@@ -589,7 +602,7 @@ Definition print_cst (prefix : string)
   | Some cst_body =>
     (* NOTE: ignoring the path part *)
     let (_, decl_name) := kn in
-    print_decl prefix TT Σ decl_name None id cst.(ExAst.cst_type).2 cst_body
+    print_decl prefix TT Σ decl_name None id cst.(ExAst.cst_type) cst_body
   | None => ""
   end.
 
@@ -608,9 +621,10 @@ Definition print_global_decl (prefix : string) (TT : MyEnv.env string)
   | TypeAliasDecl (Some (params, ty)) =>
     let ta_nm := from_option (lookup TT (string_of_kername nm))
                              (prefix ++ nm.2) in
-    (nm, "type " ++ uncapitalize ta_nm
-                 ++ concat " " (map (string_of_name ∘ tvar_name) params) ++  " = "
-            ++ print_box_type prefix TT ty)
+    (nm, "type " ++ parens (Nat.ltb #|params| 1) (concat "," (mapi (fun i v => print_type_var v.(tvar_name) i) params))
+                 ++ " " ++ uncapitalize ta_nm
+                 ++  " = "
+            ++ print_box_type prefix TT (map tvar_name params) ty)
   | TypeAliasDecl None => (nm, "")
   end.
 
diff --git a/extraction/theories/LiquidityExtract.v b/extraction/theories/LiquidityExtract.v
index 0d2c29ab..4b6d0875 100644
--- a/extraction/theories/LiquidityExtract.v
+++ b/extraction/theories/LiquidityExtract.v
@@ -10,14 +10,14 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping
 
 From MetaCoq.Template Require Pretty.
 
-From ConCert.Execution Require Import Blockchain Serializable.
+From ConCert.Execution Require Import Blockchain Serializable Common.
 
 From ConCert.Embedding Require Import MyEnv.
 From ConCert.Embedding Require Import Notations.
 From ConCert.Embedding Require Import SimpleBlockchain.
 
 From ConCert.Extraction Require Import LPretty
-     Common ExAst Erasure Optimize Extraction CertifyingInlining Certifying SpecializeChainBase.
+     Common ExAst Erasure Optimize Extraction CertifyingInlining CertifyingBeta Certifying SpecializeChainBase.
 
 From Coq Require Import List Ascii String.
 Local Open Scope string_scope.
@@ -50,6 +50,15 @@ Arguments lmd_init_prelude {_ _ _ _ _}.
 Arguments lmd_receive {_ _ _ _ _}.
 Arguments lmd_entry_point {_ _ _ _ _}.
 
+(* We override masks for *some* constants that have only logical parameters, like
+   [@AddressMap.empty]. Our optimisation conservatively keeps one parameter
+   if all the parameters are logical. This is necessary because such definitions
+   might use something like [false_rect] and removing all the arguments will force evaluating their bodies, which can lead to an exception or looping depending
+   on how the elimination from the empty types is implemented.
+   However, for [AddressMap.empty] is completely safe to remove all arguments, since it's an abbreviation for a constructor.*)
+Definition overridden_masks (kn : kername) : option bitmask :=
+  if eq_kername kn <%% @AddressMap.empty %%> then Some [true]
+  else None.
 
 (* Extract an environment with some minimal checks. This assumes the environment
    is well-formed (to make it computable from within Coq) but furthermore checks that the
@@ -64,7 +73,9 @@ Definition extract_liquidity_within_coq (to_inline : kername -> bool)
      pcuic_args :=
        {| optimize_prop_discr := true;
           extract_transforms :=
-            [dearg_transform (fun _ => None) true true true true true ] |} |}.
+            [dearg_transform overridden_masks true true true true true ]
+       |}
+  |}.
 
 Definition extract (to_inline :  kername -> bool)
            (seeds : KernameSet.t)
@@ -119,7 +130,6 @@ Definition printLiquidityDefs := printLiquidityDefs_ extract.
 (* printing *with* chainbase specialization *)
 Definition printLiquidityDefs_specialize := printLiquidityDefs_ extract_specialize.
 
-
 Definition liquidity_ignore_default :=
   [
     <%% prod %%>
diff --git a/extraction/theories/Optimize.v b/extraction/theories/Optimize.v
index 9f87192f..2f7cb2ac 100644
--- a/extraction/theories/Optimize.v
+++ b/extraction/theories/Optimize.v
@@ -412,6 +412,11 @@ Fixpoint debox_box_type_aux (args : list box_type) (bt : box_type) : box_type :=
   | TApp ty1 ty2 =>
     debox_box_type_aux (debox_box_type_aux [] ty2 :: args) ty1
   | TInd ind => dearg_single_bt (get_inductive_tvars ind) bt args
+  | TConst kn => match lookup_env Σ kn with
+                | Some (TypeAliasDecl (Some (vs, ty))) =>
+                  dearg_single_bt vs bt args
+                | _ => bt
+                end
   | _ => mkTApps bt args
   end.
 
@@ -450,7 +455,8 @@ Definition debox_type_decl (decl : global_decl) : global_decl :=
   | InductiveDecl mib => InductiveDecl (debox_type_mib mib)
   | TypeAliasDecl ta => match ta with
                        | Some (ty_vars, ty) =>
-                         TypeAliasDecl (Some (ty_vars, debox_box_type ty))
+                         TypeAliasDecl (Some (filter keep_tvar ty_vars,
+                                              reindex ty_vars (debox_box_type ty)))
                        | None => TypeAliasDecl None
                        end
   end.