diff --git a/doc/formalization/Catala.LambdaCalculus.fst b/doc/formalization/Catala.LambdaCalculus.fst
index b424d96e..8b476b65 100644
--- a/doc/formalization/Catala.LambdaCalculus.fst
+++ b/doc/formalization/Catala.LambdaCalculus.fst
@@ -31,6 +31,7 @@ type exp =
   | EVar : v: var -> exp
   | EApp : fn: exp -> arg: exp -> tau_arg: ty -> exp
   | EAbs : vty: ty -> body: exp -> exp
+  | EThunk : body:exp -> exp
   | ELit : l: lit -> exp
   | EIf : test: exp -> btrue: exp -> bfalse: exp -> exp
   | ESome : s:exp -> exp
@@ -51,7 +52,7 @@ let e_err = ELit (LError EmptyError)
 val is_value: exp -> Tot bool
 let rec is_value e =
   match e with
-  | EAbs _ _ | ELit _ | ENone -> true
+  | EAbs _ _ | EThunk _ | ELit _ | ENone -> true
   | ESome (ELit (LError _)) -> false
   | ESome e' -> is_value e'
   | EList l -> is_value_list l
@@ -86,6 +87,7 @@ let rec subst (s: var_to_exp) (e: exp) : Pure exp
   match e with
   | EVar x -> s x
   | EAbs t e1 -> EAbs t (subst (subst_abs s) e1)
+  | EThunk e1 -> EThunk (subst s e1)
   | EApp e1 e2 tau_arg -> EApp (subst s e1) (subst s e2) tau_arg
   | ELit l -> ELit l
   | EIf e1 e2 e3 -> EIf (subst s e1) (subst s e2) (subst s e3)
@@ -136,6 +138,7 @@ let rec step_app (e: exp) (e1: exp{e1 << e}) (e2: exp{e2 << e}) (tau_arg: ty{tau
         | _ -> begin
           match e1 with
           | EAbs t e' -> Some (subst (var_to_exp_beta e2) e') (* D-Beta *)
+          | EThunk e' -> Some e'
           | _ -> None
         end
       else
@@ -305,6 +308,10 @@ let rec typing (g: env) (e: exp) (tau: ty) : Tot bool (decreases (e)) =
       | TArrow tau_in tau_out -> t = tau_in &&
         typing (extend g t) e1 tau_out
       | _ -> false)
+  | EThunk e1 ->
+    (match tau with
+      | TArrow TUnit tau_out -> typing g e1 tau_out
+      | _ -> false)
   | EApp e1 e2 tau_arg -> typing g e1 (TArrow tau_arg tau) && typing g e2 tau_arg
   | ELit LTrue -> tau = TBool
   | ELit LFalse -> tau = TBool
@@ -362,10 +369,12 @@ let typing_conserved_by_list_reduction (g: env) (subs: list exp) (tau: ty)
 
 (**** Progress theorem *)
 
-let rec size_for_progress (e: exp) : Tot pos = match e with
+let rec size_for_progress (e: exp) : Tot pos =
+  match e with
   | EVar _ -> 1
   | EApp fn arg _ -> size_for_progress fn + size_for_progress arg + 1
   | EAbs _ body -> size_for_progress body + 1
+  | EThunk body -> size_for_progress body + 1
   | ELit _ -> 1
   | EIf e1 e2 e3 -> size_for_progress e1 + size_for_progress e2 + size_for_progress e3 + 1
   | ESome s -> size_for_progress s + 1
@@ -497,7 +506,6 @@ let rec progress (e: exp) (tau: ty)
      end
   end
   | _ -> ()
-
 and progress_list
   (e: exp)
   (l: list exp{size_for_progress_list l < size_for_progress e /\ l << e}) (tau: ty)
@@ -528,6 +536,7 @@ let rec substitution_extensionnal
   match e with
   | EVar _ -> ()
   | ELit _ -> ()
+  | EThunk e1 -> substitution_extensionnal s1 s2 e1
   | EAbs t e1 ->
     assert (subst s1 (EAbs t e1) == EAbs t (subst (subst_abs s1) e1))
       by (T.norm [zeta; iota; delta_only [`%subst]]);
@@ -591,6 +600,12 @@ let rec substitution_preserves_typing
   | EApp e1 e2 t_arg ->
     substitution_preserves_typing g1 e1 (TArrow t_arg t) s g2 s_lemma;
     substitution_preserves_typing g1 e2 t_arg s g2 s_lemma
+  | EThunk e1 -> begin
+    match t with
+    | TArrow TUnit t_out ->
+      substitution_preserves_typing g1 e1 t_out s g2 s_lemma
+    | _ -> ()
+  end
   | EAbs t_arg e1 -> begin
     match t with
     | TArrow t_arg' t_out ->
@@ -736,22 +751,24 @@ and preservation_list
 let identity_var_to_exp : var_to_exp = fun x -> EVar x
 
 let rec subst_by_identity_is_identity (e: exp) : Lemma (subst identity_var_to_exp e == e) =
-  match e with 
+  match e with
   | EVar _ -> ()
   | ELit _ -> ()
-  | EApp e1 e2 _ -> 
+  | EApp e1 e2 _ ->
     subst_by_identity_is_identity e1;
     subst_by_identity_is_identity e2
+  | EThunk e1 ->
+    subst_by_identity_is_identity e1
   | EAbs t e1 ->
     subst_by_identity_is_identity e1
   | ENone -> ()
-  | ESome e1 -> 
+  | ESome e1 ->
     subst_by_identity_is_identity e1
   | EIf e1 e2 e3 ->
     subst_by_identity_is_identity e1;
     subst_by_identity_is_identity e2;
     subst_by_identity_is_identity e3
-  | EList l -> 
+  | EList l ->
     subst_by_identity_is_identity_list l
   | ECatchEmptyError to_try catch_with ->
     subst_by_identity_is_identity to_try;
@@ -766,7 +783,7 @@ let rec subst_by_identity_is_identity (e: exp) : Lemma (subst identity_var_to_ex
     subst_by_identity_is_identity some
 and subst_by_identity_is_identity_list (l: list exp) : Lemma (subst_list identity_var_to_exp l == l)
   =
-  match l with 
+  match l with
   | [] -> ()
   | hd::tl ->
     subst_by_identity_is_identity hd;
@@ -779,7 +796,7 @@ let typing_empty_can_be_extended (e: exp) (tau: ty)  (tau': ty)
       (ensures (typing (extend empty tau') e tau))
   =
   subst_by_identity_is_identity e;
-  let s_lemma : subst_typing identity_var_to_exp empty (extend empty tau') = fun x -> () in 
+  let s_lemma : subst_typing identity_var_to_exp empty (extend empty tau') = fun x -> () in
   substitution_preserves_typing empty e tau identity_var_to_exp (extend empty tau') s_lemma
 
 let is_error (e: exp) : bool = match e with ELit (LError _) -> true | _ -> false
diff --git a/doc/formalization/Catala.Translation.fst b/doc/formalization/Catala.Translation.fst
index 9e966f48..589ce810 100644
--- a/doc/formalization/Catala.Translation.fst
+++ b/doc/formalization/Catala.Translation.fst
@@ -82,7 +82,7 @@ let rec translate_exp (e: D.exp) : Tot L.exp = match e with
 and translate_exp_list (l: list D.exp) : Tot (list L.exp) =
   match l with
   | [] -> []
-  | hd::tl -> (L.EAbs L.TUnit (L.subst L.increment (translate_exp hd)))::(translate_exp_list tl)
+  | hd::tl -> (L.EThunk (translate_exp hd))::(translate_exp_list tl)
 
 let translate_env (g: D.env) : Tot L.env =
  FunctionalExtensionality.on_dom L.var
@@ -201,9 +201,7 @@ and translation_preserves_typ_exceptions
     let thunked_tau' = L.TArrow L.TUnit tau' in
     assert(L.typing_list g' tl' thunked_tau');
     assert(L.typing g' hd' tau');
-    assert(L.typing g' hd' tau');
-    L.substitution_preserves_typing g' hd' tau' L.increment (L.extend g' L.TUnit) (fun x -> ());
-    assert(L.typing g' (L.EAbs L.TUnit (L.subst L.increment hd')) thunked_tau')
+    assert(L.typing g' (L.EThunk hd') thunked_tau')
 #pop-options
 
 let translation_preserves_empty_typ (e: D.exp) (tau: D.ty) : Lemma
@@ -281,6 +279,7 @@ let rec l_values_dont_step (e: L.exp) : Lemma
   =
   match e with
   | L.EAbs _ _ -> ()
+  | L.EThunk _ -> ()
   | L.ELit _ -> ()
   | L.ENone -> ()
   | L.EList [] -> ()
@@ -334,98 +333,6 @@ let process_exceptions_untouched_by_subst (s: L.var_to_exp) (tau: L.ty) : Lemma
 
 let translate_var_to_exp (s: D.var_to_exp) : Tot L.var_to_exp = fun x -> translate_exp (s x)
 
-let double_increment : L.var_to_exp = fun y -> L.EVar (y + 2)
-
-let subst_abs_increment (x: L.var) =
-  if x = 0 then L.EVar 0 else L.EVar (x + 1)
-
-let dual_substitution_commutation_weakened
-  (s : L.var_to_exp{s 0 == L.EVar 0})
-  (e: L.exp)
-    : Lemma (L.subst subst_abs_increment (L.subst s e) ==
-      L.subst (L.subst_abs s) (L.subst subst_abs_increment e))
-  =
-  admit() // TODO
-
-let substitution_commutation_bonanza
-  (s: L.var_to_exp)
-  (e: L.exp)
-    : Lemma (L.subst (L.subst_abs L.increment) (L.subst (L.subst_abs s) e) ==
-      L.subst (L.subst_abs (L.subst_abs s)) (L.subst (L.subst_abs L.increment) e))
-  =
-  let aux (x: L.var) : Lemma ((L.subst_abs L.increment) x == subst_abs_increment x) = () in
-  Classical.forall_intro aux;
-  dual_substitution_commutation_weakened (L.subst_abs s) e
-
-#push-options "--fuel 3 --ifuel 1 --z3rlimit 40"
-let rec substitution_correctness_for_exception_thunking
-  (s: L.var_to_exp)
-  (e: L.exp)
-    : Lemma (
-      (L.EAbs L.TUnit (L.subst L.increment (L.subst s e))) ==
-      (L.subst s (L.EAbs L.TUnit (L.subst L.increment e)))
-    )
-  =
-  match e with
-  | L.EVar _ -> ()
-  | L.EAbs t body ->
-    // Top to down
-    assert(L.subst s e == L.EAbs t (L.subst (L.subst_abs s) body));
-    assert(L.subst L.increment (L.subst s e) ==
-      L.EAbs t (L.subst (L.subst_abs L.increment) (L.subst (L.subst_abs s) body)));
-    assert(L.EAbs L.TUnit (L.subst L.increment (L.subst s e)) ==
-      L.EAbs L.TUnit
-        (L.EAbs t (L.subst (L.subst_abs L.increment) (L.subst (L.subst_abs s) body))));
-    // Down to top
-    assert(L.subst L.increment e == L.EAbs t (L.subst (L.subst_abs L.increment) body));
-    assert(L.EAbs L.TUnit (L.subst L.increment e) ==
-      L.EAbs L.TUnit (L.EAbs t (L.subst (L.subst_abs L.increment) body)));
-    assert(L.subst s (L.EAbs L.TUnit (L.subst L.increment e)) ==
-      L.EAbs L.TUnit
-        (L.subst (L.subst_abs s) (L.EAbs t (L.subst (L.subst_abs L.increment) body))));
-    assert(L.subst s (L.EAbs L.TUnit (L.subst L.increment e)) ==
-      L.EAbs L.TUnit
-        (L.EAbs t
-          (L.subst (L.subst_abs (L.subst_abs s)) (L.subst (L.subst_abs L.increment) body))));
-    substitution_commutation_bonanza s body
-  | L.EApp e1 e2 _ ->
-    substitution_correctness_for_exception_thunking s e1;
-    substitution_correctness_for_exception_thunking s e2
-  | L.ELit _ -> ()
-  | L.EIf e1 e2 e3 ->
-    substitution_correctness_for_exception_thunking s e1;
-    substitution_correctness_for_exception_thunking s e2;
-    substitution_correctness_for_exception_thunking s e3
-  | L.ESome e1 -> substitution_correctness_for_exception_thunking s e1
-  | L.ENone -> ()
-  | L.EMatchOption e1 _ e2 e3 ->
-    substitution_correctness_for_exception_thunking s e1;
-    substitution_correctness_for_exception_thunking s e2;
-    substitution_correctness_for_exception_thunking s e3
-  | L.ECatchEmptyError e1 e2 ->
-    substitution_correctness_for_exception_thunking s e1;
-    substitution_correctness_for_exception_thunking s e2
-  | L.EFoldLeft e1 e2 _ e3 _ ->
-    substitution_correctness_for_exception_thunking s e1;
-    substitution_correctness_for_exception_thunking s e2;
-    substitution_correctness_for_exception_thunking s e3
-  | L.EList l ->
-    substitution_correctness_for_exception_thunking_list s l
-and substitution_correctness_for_exception_thunking_list
-  (s: L.var_to_exp)
-  (l: list L.exp)
-    : Lemma (
-      (L.EAbs L.TUnit (L.subst L.increment (L.subst s (L.EList l)))) ==
-      (L.subst s (L.EAbs L.TUnit (L.subst L.increment (L.EList l))))
-    )
-  =
-  match l with
-  | [] -> ()
-  | hd::tl ->
-    substitution_correctness_for_exception_thunking s hd;
-    substitution_correctness_for_exception_thunking_list s tl
-#pop-options
-
 #push-options "--fuel 3 --ifuel 1 --z3rlimit 50"
 let rec substitution_correctness (s: D.var_to_exp) (e: D.exp)
     : Lemma (ensures (
@@ -462,8 +369,7 @@ and substitution_correctness_list (s: D.var_to_exp) (l: list D.exp)
  | hd::tl ->
    let s' = translate_var_to_exp s in
    substitution_correctness_list s tl;
-   substitution_correctness s hd;
-   substitution_correctness_for_exception_thunking s' (translate_exp hd)
+   substitution_correctness s hd
 and translate_var_to_exp_abs_commute (s: D.var_to_exp)
     : Lemma
       (ensures (
@@ -789,10 +695,6 @@ let process_exceptions_applied_stepping
     : Lemma (take_l_steps (L.TOption tau) (process_exceptions_applied tau acc hd) 3 ==
       Some (process_exceptions_applied_stepped tau acc hd))
   =
-  let e = 1 in
-  let e' = 2 in
-  let a' = 3 in
-  let e'' = 4 in
   let e1 : L.exp =
     L.EApp
       (L.EAbs (L.TArrow L.TUnit tau) (
@@ -805,11 +707,11 @@ let process_exceptions_applied_stepping
             (L.EAbs tau (L.ELit (L.LError L.ConflictError)))
         ))
     ))
-    (L.ECatchEmptyError (L.ESome (L.EApp (L.EVar e) (L.ELit L.LUnit) L.TUnit)) L.ENone)
+    (L.ECatchEmptyError (L.ESome (L.EApp (L.EVar 0) (L.ELit L.LUnit) L.TUnit)) L.ENone)
     (L.TOption tau)
   )
       )
-      (L.EAbs L.TUnit hd) (L.TArrow L.TUnit tau)
+      (L.EThunk hd) (L.TArrow L.TUnit tau)
   in
   let e2 =
     L.EApp (L.EAbs (L.TOption tau) (
@@ -821,12 +723,12 @@ let process_exceptions_applied_stepping
             (L.EAbs tau (L.ELit (L.LError L.ConflictError)))
         ))
     ))
-    (L.ECatchEmptyError (L.ESome (L.EApp (L.EAbs L.TUnit hd) (L.ELit L.LUnit) L.TUnit)) L.ENone)
+    (L.ECatchEmptyError (L.ESome (L.EApp (L.EThunk hd) (L.ELit L.LUnit) L.TUnit)) L.ENone)
     (L.TOption tau)
 
   in
   assume(L.step (process_exceptions_applied tau acc hd) == Some e1);
-  assume(L.step e1 == Some e2);
+  assert(L.step e1 == Some e2);
   admit()
 #pop-options
 
@@ -843,16 +745,14 @@ let lift_multiple_l_steps_exceptions_head
     : Lemma
       (requires (take_l_steps tau hd n_hd == Some final_hd /\ L.is_value acc))
       (ensures (
-        L.typing_empty_can_be_extended hd tau L.TUnit;
         build_default_translation_typing
-          ((L.EAbs L.TUnit hd)::tl) acc just cons tau L.empty;
+          ((L.EThunk hd)::tl) acc just cons tau L.empty;
         take_l_steps tau
-          (build_default_translation ((L.EAbs L.TUnit hd)::tl) acc just cons tau)
+          (build_default_translation ((L.EThunk hd)::tl) acc just cons tau)
           (n_hd + 4) ==
             Some (exceptions_head_lift tau tl acc just cons final_hd)))
   =
-  L.typing_empty_can_be_extended hd tau L.TUnit;
-  build_default_translation_typing ((L.EAbs L.TUnit hd)::tl) acc just cons tau L.empty;
+  build_default_translation_typing ((L.EThunk hd)::tl) acc just cons tau L.empty;
   let e' = 2 in
   let a' = 3 in
   let e'' = 4 in
@@ -866,10 +766,10 @@ let lift_multiple_l_steps_exceptions_head
   in
   let init = L.EApp
     (L.EApp (process_exceptions_f tau) acc (L.TOption tau))
-    (L.EAbs L.TUnit hd) (L.TArrow L.TUnit tau)
+    (L.EThunk hd) (L.TArrow L.TUnit tau)
   in
-  let open FStar.Tactics in
   admit();
+  let open FStar.Tactics in
   assert(take_l_steps (L.TOption tau) init 3 == Some init_stepped) by begin
     compute ()
   end;
@@ -1016,6 +916,7 @@ let rec translation_correctness_exceptions_left_to_right_step
         let ltau = translate_ty dtau in
         translation_preserves_empty_typ de' dtau;
         admit();
+        build_default_translation_typing lcurrent L.ENone ljust lcons ltau L.empty;
         take_l_steps ltau (build_default_translation lcurrent L.ENone ljust lcons ltau)
           n1 == Some target_e /\
         take_l_steps ltau le' n2 == Some target_e