diff --git a/INSTALL.md b/INSTALL.md
index a550810ef..334ffae8e 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -72,12 +72,12 @@ To setup a fresh `opam` installation, you might want to create a
 one yet. You need to use **opam 2** to obtain the right version of
 `Equations`.
 
-    # opam switch create coq.8.14 4.07.1
+    # opam switch create coq.8.16 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda
     # eval $(opam env)
 
-This creates the `coq.8.14` switch which initially contains only the
-basic `OCaml` `4.07.1` compiler, and puts you in the right environment
-(check with `ocamlc -v`).
+This creates the `coq.8.16` switch which initially contains only the
+basic `OCaml` `4.13.1` compiler with the `flambda` option enabled,
+and puts you in the right environment (check with `ocamlc -v`).
 
 Once in the right switch, you can install `Coq` and the `Equations` package using:
 
diff --git a/Makefile b/Makefile
index be78882f1..337ddc9da 100644
--- a/Makefile
+++ b/Makefile
@@ -119,7 +119,7 @@ ci-local-noclean:
 	./configure.sh local
 	$(MAKE) all test-suite TIMED=pretty-timed
 
-ci-local: ci-local-noclean
+ci-local: ci-local-noclean 
 	$(MAKE) clean
 
 ci-quick:
@@ -130,3 +130,6 @@ ci-opam:
 # Use -v so that regular output is produced
 	opam install -v -y .
 	opam remove -y coq-metacoq coq-metacoq-template
+
+checktodos:
+	sh checktodos.sh
diff --git a/README.md b/README.md
index 84d958dad..ed7351f25 100644
--- a/README.md
+++ b/README.md
@@ -54,9 +54,14 @@ Template-Coq with additional features. Each extension is in dedicated folder.
 
 Template-Coq is a quoting library for [Coq](http://coq.inria.fr). It
 takes `Coq` terms and constructs a representation of their syntax tree as
-a `Coq` inductive data type. The representation is based on the kernel's
+an inductive data type. The representation is based on the kernel's
 term representation.
 
+After importing `MetaCoq.Template.Loader` there are commands `MetaCoq Test Quote t.`, 
+`MetaCoq Quote Definition name := (t).` and `MetaCoq Quote Recursively Definition name := (t).` as 
+well as a tactic `quote_term t k`,
+where in all cases `t` is a term and `k` a continuation tactic.
+
 In addition to this representation of terms, Template Coq includes:
 
 - Reification of the environment structures, for constant and inductive
@@ -66,9 +71,9 @@ In addition to this representation of terms, Template Coq includes:
 
 - A monad for manipulating global declarations, calling the type
   checker, and inserting them in the global environment, in
-  the style of MTac.
+  the style of MTac. Monadic programs `p : TemplateMonad A` can be run using `MetaCoq Run p`.
 
-- A formalisation of the expected typing rules reflecting the ones of Coq
+- A formalisation of the typing rules reflecting the ones of Coq, not covering eta-expansion and template polymorphism.
 
 ### [PCUIC](https://github.com/MetaCoq/metacoq/tree/coq-8.11/pcuic)
 
@@ -92,6 +97,13 @@ calculus has proofs of standard metatheoretical results:
   that singleton elimination (from Prop to Type) is only allowed
   on singleton inductives in Prop.
 
+- Canonicity: The weak head normal form of erms of inductive type is a constructor application.
+
+- Consistency under the assumption of strong normalization
+  
+- Weak call-by-value standardization: Normal forms of terms of first-order inductive type
+can be found via weak call-by-value evaluation.
+
 ### [Safe Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.16/safechecker)
 
 Implementation of a fuel-free and verified reduction machine, conversion
@@ -108,12 +120,11 @@ type-checker, one can use:
 
     MetaCoq CoqCheck <term>
 
-
 ### [Erasure](https://github.com/MetaCoq/metacoq/tree/coq-8.16/erasure)
 
 An erasure procedure to untyped lambda-calculus accomplishing the
-same as the Extraction plugin of Coq. The extracted safe erasure is
-available in Coq through a new vernacular command:
+same as the type and proof erasure phase of the Extraction plugin of Coq.
+The extracted safe erasure is available in Coq through a new vernacular command:
 
     MetaCoq Erase <term>
 
@@ -138,8 +149,6 @@ Examples of translations built on top of this:
   and [test-suite/safechecker_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.16/test-suite/safechecker_test.v) show example
   uses (and current limitations of) the verified checker and erasure.
 
-
-
 ## Papers
 
 - ["Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq"](https://metacoq.github.io/coqcoqcorrect)
diff --git a/RELEASING.md b/RELEASING.md
index 91e4c35e3..4d2613a6d 100644
--- a/RELEASING.md
+++ b/RELEASING.md
@@ -1 +1,2 @@
 - Change the "version:" fields in opam files.
+
diff --git a/checktodos.sh b/checktodos.sh
new file mode 100755
index 000000000..25b2476f3
--- /dev/null
+++ b/checktodos.sh
@@ -0,0 +1,21 @@
+#!/bin/sh
+
+if [[ $(git grep -c todo | grep theories) = template-coq/theories/utils/MCUtils.v:3 ]]
+then
+    echo "No todos found"
+    if [[ $(git grep -c Admitted | grep theories) = "" ]]
+    then
+        echo "No Admitted results found"
+        exit 0
+    else
+        echo "Found Admitted results:"
+        git grep -c Admitted | grep theories
+        exit 1
+    fi
+else
+    echo "Found todos:"
+    git grep -c todo | grep theories
+    exit 1
+fi
+endef
+
diff --git a/erasure/theories/EArities.v b/erasure/theories/EArities.v
index b7dbf552b..f687356d5 100644
--- a/erasure/theories/EArities.v
+++ b/erasure/theories/EArities.v
@@ -22,7 +22,7 @@ Local Existing Instance extraction_checker_flags.
 
 Implicit Types (cf : checker_flags) (Σ : global_env_ext).
 
-(* todo move *)
+(* TODO move *)
 #[global] Existing Instance extends_refl.
 
 Lemma isErasable_Proof Σ Γ t :
diff --git a/erasure/theories/Erasure.v b/erasure/theories/Erasure.v
index 11ff060f7..f3f570c61 100644
--- a/erasure/theories/Erasure.v
+++ b/erasure/theories/Erasure.v
@@ -108,20 +108,32 @@ Definition run_erase_program_fast {guard : abstract_guard_impl} := run erasure_p
 
 Local Open Scope string_scope.
 
+Axiom fake_guard_impl_properties : 
+forall (fix_cofix: PCUICTyping.FixCoFix)
+       (Σ: PCUICAst.PCUICEnvironment.global_env_ext)
+       (Γ: PCUICAst.PCUICEnvironment.context)
+       (mfix: BasicAst.mfixpoint PCUICAst.term),
+PCUICTyping.guard fix_cofix Σ Γ mfix <-> fake_guard_impl fix_cofix Σ Γ mfix.
+
+
 Global Program Instance fake_guard_impl : abstract_guard_impl :=
 {| guard_impl := fake_guard_impl |}.
-Next Obligation. Admitted.  
+Next Obligation. apply fake_guard_impl_properties. Qed.
 
 (** This uses the retyping-based erasure and assumes that the global environment and term 
   are welltyped (for speed). As such this should only be used for testing, or when we know that 
   the environment is wellformed and the term well-typed (e.g. when it comes directly from a 
   Coq definition). *)
+
+
+Axiom assume_that_we_only_erase_on_welltyped_programs :
+  forall (p : Ast.Env.program), squash (TemplateProgram.wt_template_program p).
 Definition erase_and_print_template_program {cf : checker_flags} (p : Ast.Env.program)
   : string :=
-  let p' := run_erase_program p (sq (todo "assuming quoted environment and term are well-typed")) in
+  let p' := run_erase_program p (assume_that_we_only_erase_on_welltyped_programs p) in
   time "Pretty printing" EPretty.print_program p'.
 
 Program Definition erase_fast_and_print_template_program {cf : checker_flags} (p : Ast.Env.program)
   : string :=
-  let p' := run_erase_program_fast p (sq (todo "wf_env and welltyped term")) in
+  let p' := run_erase_program_fast p (assume_that_we_only_erase_on_welltyped_programs p) in
   time "pretty-printing" EPretty.print_program p'.
diff --git a/pcuic/theories/PCUICEquality.v b/pcuic/theories/PCUICEquality.v
index ff3b500b6..cdef24b7d 100644
--- a/pcuic/theories/PCUICEquality.v
+++ b/pcuic/theories/PCUICEquality.v
@@ -1291,7 +1291,7 @@ Proof.
   eapply eq_term_upto_univ_trans; exact _.
 Qed.
 
-(* todo: rename *)
+(* TODO: rename *)
 (* Definition nleq_term t t' := *)
 (*   eqb_term_upto_univ eqb eqb t t'. *)
 
diff --git a/pcuic/theories/PCUICInversion.v b/pcuic/theories/PCUICInversion.v
index b97fc475d..90020982d 100644
--- a/pcuic/theories/PCUICInversion.v
+++ b/pcuic/theories/PCUICInversion.v
@@ -6,7 +6,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICCases PCUICLiftSubst PCUICUnivSu
      PCUICOnFreeVars PCUICClosedTyp PCUICWellScopedCumulativity.
 
 Require Import Equations.Prop.DepElim.
-(* todo: make wf arguments implicit *)
+(* TODO: make wf arguments implicit *)
 Section Inversion.
 
   Context {cf : checker_flags}.
diff --git a/pcuic/theories/PCUICSafeLemmata.v b/pcuic/theories/PCUICSafeLemmata.v
index 92f2d72b7..bf439d604 100644
--- a/pcuic/theories/PCUICSafeLemmata.v
+++ b/pcuic/theories/PCUICSafeLemmata.v
@@ -346,7 +346,7 @@ Section Lemmata.
     destruct h; depelim wf; simpl in *.
     all: destruct l; econstructor; eauto.
   Qed.
-  (* todo: rename alpha_eq *)
+  (* TODO: rename alpha_eq *)
   Lemma compare_decls_conv Γ Γ' :
     eq_context_upto_names Γ Γ' ->
     conv_context cumulAlgo_gen Σ Γ Γ'.
diff --git a/pcuic/theories/utils/PCUICAstUtils.v b/pcuic/theories/utils/PCUICAstUtils.v
index b91b6b3b7..006243ec1 100644
--- a/pcuic/theories/utils/PCUICAstUtils.v
+++ b/pcuic/theories/utils/PCUICAstUtils.v
@@ -205,7 +205,7 @@ Fixpoint remove_arity (n : nat) (t : term) : term :=
   | O => t
   | S n => match t with
           | tProd _ _ B => remove_arity n B
-          | _ => t (* todo *)
+          | _ => t (* TODO *)
           end
   end.
 
@@ -282,7 +282,7 @@ Fixpoint decompose_prod_n_assum (Γ : context) n (t : term) : option (context *
     end
   end.
 
-(* todo move *)
+(* TODO move *)
 Lemma it_mkLambda_or_LetIn_app l l' t :
   it_mkLambda_or_LetIn (l ++ l') t = it_mkLambda_or_LetIn l' (it_mkLambda_or_LetIn l t).
 Proof. induction l in l', t |- *; simpl; auto. Qed.
@@ -402,7 +402,7 @@ Ltac merge_All :=
 #[global]
 Hint Rewrite @map_def_id @map_id : map.
 
-(* todo move *)
+(* TODO move *)
 Ltac close_All :=
   match goal with
   | H : Forall _ _ |- Forall _ _ => apply (Forall_impl H); clear H; simpl
diff --git a/safechecker/theories/Extraction.v b/safechecker/theories/Extraction.v
index b269dda4f..03ffbfcf5 100644
--- a/safechecker/theories/Extraction.v
+++ b/safechecker/theories/Extraction.v
@@ -37,12 +37,19 @@ Extraction Inline Equations.Prop.Logic.True_rect_dep Equations.Prop.Logic.False_
 Extraction Inline PCUICPrimitive.prim_val_reflect_eq.
 
 Cd "src".
+Axiom fake_abstract_guard_impl_properties:
+  forall (fix_cofix : PCUICTyping.FixCoFix)
+    (Σ : PCUICAst.PCUICEnvironment.global_env_ext)
+    (Γ : PCUICAst.PCUICEnvironment.context)
+    (mfix : BasicAst.mfixpoint PCUICAst.term),
+    PCUICTyping.guard fix_cofix Σ Γ mfix <->
+      PCUICWfEnvImpl.fake_guard_impl fix_cofix Σ Γ mfix.
 
 #[local,program] Instance fake_abstract_guard_impl : PCUICWfEnvImpl.abstract_guard_impl := 
   {
     guard_impl := PCUICWfEnvImpl.fake_guard_impl
   }.
-Next Obligation. Admitted. 
+Next Obligation. eapply fake_abstract_guard_impl_properties. Qed.
 
 Definition infer_and_print_template_program_with_guard {cf} {nor} := 
   @SafeTemplateChecker.infer_and_print_template_program cf nor fake_abstract_guard_impl.
diff --git a/safechecker/theories/PCUICEqualityDec.v b/safechecker/theories/PCUICEqualityDec.v
index 7f48784cc..633942d43 100644
--- a/safechecker/theories/PCUICEqualityDec.v
+++ b/safechecker/theories/PCUICEqualityDec.v
@@ -13,7 +13,7 @@ Local Set Keyed Unification.
 
 Set Default Goal Selector "!".
 
-(*todo move*)
+(* TODO move*)
 
 Lemma consistent_instance_wf_universe `{checker_flags} Σ uctx u :
   consistent_instance_ext Σ uctx u ->
diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v
index b3a733b30..8fb8f19d1 100644
--- a/safechecker/theories/PCUICSafeConversion.v
+++ b/safechecker/theories/PCUICSafeConversion.v
@@ -5850,13 +5850,13 @@ match
              (LevelSet.add Level.lzero LevelSet.empty, ConstraintSet.empty);
            declarations := []
          |}, Monomorphic_ctx);
-      referenced_impl_ext_wf := todo "foo"
+      referenced_impl_ext_wf := TODO "foo"
     |} [] Cumul (tSort (Universe.lType (Universe.make' (Level.lzero, 0))))
-    (todo "") (tSort (Universe.lType (Universe.make' (Level.lzero, 0))))
-    (todo "")
+    (TODO "") (tSort (Universe.lType (Universe.make' (Level.lzero, 0))))
+    (TODO "")
 with
 | ConvSuccess => "success"
-| ConvError _ => todo "foo"
+| ConvError _ => TODO "foo"
 end = "success".
 Proof.
   lazy. reflexivity.
diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v
index 5aacad2bf..3f43d0668 100644
--- a/safechecker/theories/PCUICTypeChecker.v
+++ b/safechecker/theories/PCUICTypeChecker.v
@@ -1769,7 +1769,7 @@ Section Typecheck.
   Qed.
     
   Next Obligation.
-    (*todo: factor*)
+    (*TODO: factor*)
     cbn in *. pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq. 
     apply eqb_eq in i. subst I.
     eapply eqb_eq in i0.
diff --git a/template-coq/theories/AstUtils.v b/template-coq/theories/AstUtils.v
index 48083d574..68f1ac450 100644
--- a/template-coq/theories/AstUtils.v
+++ b/template-coq/theories/AstUtils.v
@@ -192,7 +192,7 @@ Fixpoint remove_arity (n : nat) (t : term) : term :=
   | O => t
   | S n => match t with
           | tProd _ _ B => remove_arity n B
-          | _ => t (* todo *)
+          | _ => t (* TODO *)
           end
   end.
 
diff --git a/template-coq/theories/Checker.v b/template-coq/theories/Checker.v
index 593cd815e..b6f79db53 100644
--- a/template-coq/theories/Checker.v
+++ b/template-coq/theories/Checker.v
@@ -614,25 +614,6 @@ Definition check_conv `{checker_flags} {F:Fuel} := check_conv_gen Conv.
 Definition is_graph_of_global_env_ext `{checker_flags} Σ G :=
   is_graph_of_uctx G (global_ext_uctx Σ).
 
-Lemma conv_spec : forall `{checker_flags} {F:Fuel} Σ G Γ t u,
-    is_graph_of_global_env_ext Σ G ->
-    Σ ;;; Γ |- t = u <~> check_conv (fst Σ) G Γ t u = Checked ().
-Proof.
-  intros. todo "Checker.conv_spec".
-Defined.
-
-Lemma cumul_spec : forall `{checker_flags} {F:Fuel} Σ G Γ t u,
-    is_graph_of_global_env_ext Σ G ->
-    Σ ;;; Γ |- t <= u <~> check_conv_leq (fst Σ) G Γ t u = Checked ().
-Proof.
-  intros. todo "Checker.cumul_spec".
-Defined.
-
-Lemma reduce_cumul :
-  forall `{checker_flags} Σ Γ n t, Σ ;;; Γ |- try_reduce (fst Σ) Γ n t <= t.
-Proof. intros. todo "Checker.reduce_cumul". Defined.
-
-
 Section Typecheck.
   Context {F : Fuel}.
   Context (Σ : global_env).
diff --git a/template-coq/theories/EnvMap.v b/template-coq/theories/EnvMap.v
index b9f1389d1..d7b39028f 100644
--- a/template-coq/theories/EnvMap.v
+++ b/template-coq/theories/EnvMap.v
@@ -293,7 +293,7 @@ Context {A : Type}.
   Lemma pos_of_string_cont_inj s s' p : pos_of_string_cont s p = pos_of_string_cont s' p -> s = s'.
   Proof.
     induction s; destruct s' => /= //.
-  Admitted.
+  Qed.                          (* TODO *)
   
   Fixpoint pos_of_dirpath_cont (d : dirpath) (cont : positive) : positive := 
     match d with
@@ -324,7 +324,7 @@ Context {A : Type}.
     induction a; destruct m => /= //.
 
     cbn.
-  Admitted.
+  Qed.                          (* TODO *)
 
   Definition empty : t := PTree.empty _.
 
diff --git a/template-coq/theories/LiftSubst.v b/template-coq/theories/LiftSubst.v
index 28f215634..5a506f748 100644
--- a/template-coq/theories/LiftSubst.v
+++ b/template-coq/theories/LiftSubst.v
@@ -461,7 +461,7 @@ Qed.
 Lemma noccur_between_subst k n t : noccur_between k n t -> 
   closedn (n + k) t -> closedn k t.
 Proof.
-Admitted. *)
+Qed.  *)                        (* TODO *)
 
 Lemma strip_casts_lift n k t : 
   strip_casts (lift n k t) = lift n k (strip_casts t).
@@ -524,4 +524,4 @@ Proof.
   pose (subst_context_snoc n k ctx a). unfold snoc in e. rewrite e. clear e.
   simpl. rewrite -> IHctx.
   pose (subst_context_snoc n k ctx a). simpl. now destruct a as [na [b|] ty].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/template-coq/theories/TemplateCheckWf.v b/template-coq/theories/TemplateCheckWf.v
index 492d0b29a..6ed3e103d 100644
--- a/template-coq/theories/TemplateCheckWf.v
+++ b/template-coq/theories/TemplateCheckWf.v
@@ -9,8 +9,11 @@ Open Scope bs_scope.
 
 Definition run_eta_program := Transform.run template_eta_expand.
 
+Axiom assume_welltypedness_of_input : forall p, ∥ wt_template_program p ∥.
 Definition eta_expand p := 
-  run_eta_program p (todo "assume well-typedness").
+  run_eta_program p (assume_welltypedness_of_input p).
+
+Compute (Transform.pre template_eta_expand _).
 
 Definition check_def (d : kername × global_decl) : TemplateMonad unit :=
   match d.2 with
@@ -72,4 +75,4 @@ Definition check_wf_eta (g : Ast.Env.program) : TemplateMonad unit :=
 
 (* To test that a program's eta-expansion is indeed well-typed according to Coq's kernel use: 
  
-  MetaCoq Run (tmQuoteRec wf_program >>= check_wf_eta). *)
\ No newline at end of file
+  MetaCoq Run (tmQuoteRec wf_program >>= check_wf_eta). *)
diff --git a/template-coq/theories/TemplateProgram.v b/template-coq/theories/TemplateProgram.v
index f243eaca5..9a1d1aba6 100644
--- a/template-coq/theories/TemplateProgram.v
+++ b/template-coq/theories/TemplateProgram.v
@@ -31,6 +31,24 @@ Definition template_expand_obseq (p p' : template_program) (v v' : Ast.term) :=
   
 Local Obligation Tactic := idtac.
 
+Axiom eta_expansion_preserves_wf_ext_and_typing :
+  forall (cf : checker_flags)
+    (Σ : global_env)
+    (t : term)
+    (wfext : wf_ext (empty_ext (Σ, t).1))
+    (ht : ∑ T : term, empty_ext (Σ, t).1;;; [] |- (Σ, t).2 : T),
+  ∥ wt_template_program (eta_expand_program (Σ, t)) ∥.
+
+Axiom eta_expansion_preserves_evaluation :
+  forall (cf : checker_flags)
+    (Σ : global_env)
+    (t v : term)
+    (w : wf_ext (empty_ext (Σ, t).1))
+    (s : ∑ T : term, empty_ext (Σ, t).1;;; [] |- (Σ, t).2 : T)
+    (ev : ∥ eval Σ t v ∥),
+    ∥ eval (eta_expand_global_env Σ) (eta_expand (declarations Σ) [] t)
+    (eta_expand (declarations Σ) [] v) ∥.
+
 Program Definition template_eta_expand {cf : checker_flags} : self_transform template_program Ast.term eval_template_program eval_template_program :=
  {| name := "eta-expansion of template program";
     pre p := ∥ wt_template_program p ∥;
@@ -39,7 +57,7 @@ Program Definition template_eta_expand {cf : checker_flags} : self_transform tem
     obseq := template_expand_obseq |}.
 Next Obligation.
   intros cf [Σ t] [[wfext ht]].
-  cbn. split. split. todo "eta-expansion preserves wf ext and typing".
+  cbn. split. eapply eta_expansion_preserves_wf_ext_and_typing; eauto.
   red.
   destruct ht as [T ht].
   split; cbn. eapply EtaExpand.eta_expand_global_env_expanded. apply wfext.
@@ -53,7 +71,7 @@ Next Obligation.
   red. intros cf [Σ t] v [[]].
   unfold eval_template_program.
   cbn. intros ev.
-  exists (EtaExpand.eta_expand (Ast.Env.declarations Σ) [] v). split. split.
-  todo "eta-expansion preserves evaluation".
+  exists (EtaExpand.eta_expand (Ast.Env.declarations Σ) [] v). split.
+  eapply eta_expansion_preserves_evaluation; eauto.
   red. reflexivity.
 Qed.
diff --git a/template-coq/theories/Universes.v b/template-coq/theories/Universes.v
index e14b89f0a..dc3de4d18 100644
--- a/template-coq/theories/Universes.v
+++ b/template-coq/theories/Universes.v
@@ -2531,7 +2531,7 @@ Definition polymorphic_instance uctx :=
   | Monomorphic_ctx => Instance.empty
   | Polymorphic_ctx c => fst (snd (AUContext.repr c))
   end.
-(* todo: duplicate of polymorphic_instance *)
+(* TODO: duplicate of polymorphic_instance *)
 Definition abstract_instance decl :=
   match decl with
   | Monomorphic_ctx => Instance.empty
diff --git a/template-coq/theories/monad_utils.v b/template-coq/theories/monad_utils.v
index 07cc7c175..dc3f08eac 100644
--- a/template-coq/theories/monad_utils.v
+++ b/template-coq/theories/monad_utils.v
@@ -1,6 +1,3 @@
-(* todo(gmm): This file should really be replaced by a real
- * monad library.
- *)
 Require Import Arith List.
 From MetaCoq.Template Require Import All_Forall MCSquash.
 From Equations Require Import Equations.
diff --git a/template-coq/theories/utils/All_Forall.v b/template-coq/theories/utils/All_Forall.v
index 4adaadac6..a6a09502b 100644
--- a/template-coq/theories/utils/All_Forall.v
+++ b/template-coq/theories/utils/All_Forall.v
@@ -1767,7 +1767,7 @@ Proof.
   move=> [= <-]. now rewrite (IHHa _ E').
 Qed.
 
-(* todo: move *)
+(* TODO: move *)
 Lemma All_mapi {A B} P f l k :
   Alli (fun i x => P (f i x)) k l -> All P (@mapi_rec A B f l k).
 Proof.