diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 0697b5e..62d48df 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -16,7 +16,7 @@ jobs:
     runs-on: ubuntu-latest
 
     env:
-      coq_version: '8.19'
+      coq_version: '8.20'
       ocaml_version: '4.14-flambda'
       fail-fast: true
 
diff --git a/coq-partialfun b/coq-partialfun
index 366e901..5919edd 160000
--- a/coq-partialfun
+++ b/coq-partialfun
@@ -1 +1 @@
-Subproject commit 366e9017248b79ab161ed12e45c10fd41d1de87d
+Subproject commit 5919eddd54339038359e2c7b2ea5363ce70c0d07
diff --git a/opam b/opam
index d5ffbe3..f96e436 100644
--- a/opam
+++ b/opam
@@ -1,4 +1,4 @@
-opam-version: "2.0"              
+opam-version: "2.0"
 version: "8.19.dev"
 maintainer: "Meven.Bertrand@univ-nantes.fr"
 dev-repo: "git+https://github.com/CoqHott/logrel-coq.git"
@@ -10,7 +10,7 @@ authors: ["Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
 ]
 license: "MIT"
 depends: [
-  "coq" { >= "8.19" & < "8.20~" }
+  "coq" { >= "8.20" & < "8.21~" }
   "coq-smpl"
   "coq-equations" { >= "1.3" }
 ]
diff --git a/theories/AlgorithmicConvProperties.v b/theories/AlgorithmicConvProperties.v
index 86fc4ef..bb5f73f 100644
--- a/theories/AlgorithmicConvProperties.v
+++ b/theories/AlgorithmicConvProperties.v
@@ -93,7 +93,7 @@ Section AlgoConvConv.
       now boundary.
     - now econstructor.
     - now econstructor.
-    - now econstructor. 
+    - now econstructor.
     - intros * ? ihA ? ihB ? h **.
       econstructor.
       1: now eapply ihA.
@@ -191,7 +191,7 @@ Section AlgoConvConv.
       eapply stability in hm' as [? [[-> ]]]%termGen'; tea.
       pose proof (redty_whnf red (isType_whnf _ isTy)); subst.
       assert [Γ' |-[de] A ≅ A] by (eapply stability; tea; now eapply lrefl).
-      assert [Γ' |-[de] x ≅ x : A] by (eapply stability; tea; now eapply lrefl). 
+      assert [Γ' |-[de] x ≅ x : A] by (eapply stability; tea; now eapply lrefl).
       assert [|- (Γ',, A),, tId A⟨@wk1 Γ' A⟩ x⟨@wk1 Γ' A⟩ (tRel 0) ≅ (Γ,, A),, tId A⟨@wk1 Γ A⟩ x⟨@wk1 Γ A⟩ (tRel 0)].
       1: eapply idElimMotiveCtxConv; first [now econstructor| now symmetry| boundary].
       assert [Γ' |-[ de ] P[tRefl A x .: x..] ≅ P[tRefl A x .: x..]].
@@ -213,7 +213,8 @@ Section AlgoConvConv.
       }
       eexists ; split.
       + econstructor.
-        1-2: eauto using redty_red.
+        1: eauto.
+        1: now eapply redty_red.
         gen_typing.
       + symmetry ; etransitivity ; tea.
         now eapply RedConvTyC.
@@ -288,14 +289,14 @@ Section AlgoConvConv.
       2: gen_typing.
       econstructor ; tea.
       eapply IHf ; tea.
-      now econstructor. 
+      now econstructor.
     - intros * ? [ihA] ? [ihB] ?????? r%red_ty_compl_univ_l wh%isType_whnf.
       pose proof (redty_whnf r wh); subst.
       econstructor.
       1: eapply ihA; tea; gen_typing.
       assert [ |-[ de ] Γ',, A ≅ Γ,, A].  1:{
-        econstructor; tea; eapply stability; tea. 
-        eapply lrefl; now econstructor. 
+        econstructor; tea; eapply stability; tea.
+        eapply lrefl; now econstructor.
       }
       eapply ihB; tea.
       do 2 constructor; boundary.
@@ -303,7 +304,7 @@ Section AlgoConvConv.
       pose proof (redty_whnf r wh); subst.
       econstructor; tea.
       1: eapply ihA; tea; now symmetry.
-      eapply ihB; tea. 
+      eapply ihB; tea.
       eapply typing_subst1; tea.
       eapply TermConv; refold; [|now symmetry].
       eapply TermRefl, stability; tea.
@@ -377,7 +378,7 @@ Section TermTypeConv.
   Let PTmEq (Γ : context) (A t u : term) :=
       [A ⤳* U] ->
       [Γ |-[al] t ≅ u].
-  Let PTmRedEq (Γ : context) (A t u : term) := 
+  Let PTmRedEq (Γ : context) (A t u : term) :=
     A = U ->
     [Γ |-[al] t ≅h u].
 
@@ -401,10 +402,10 @@ Section TermTypeConv.
       congruence.
     - intros; congruence.
     - intros; congruence.
-    - intros. 
+    - intros.
       now econstructor.
   Qed.
-  
+
 End TermTypeConv.
 
 (** ** Symmetry *)
@@ -657,7 +658,7 @@ Section Symmetry.
     - intros * ? IH **.
       econstructor.
       now eapply IH.
-    - now econstructor.  
+    - now econstructor.
     - intros * ? ? ? IH ? Hf  **.
       econstructor.
       1-2: assumption.
@@ -725,7 +726,7 @@ Section Symmetry.
       edestruct IH as [[? []] []] ; tea.
       now econstructor.
   Qed.
-  
+
 End Symmetry.
 
 (** ** Transitivity *)
@@ -770,7 +771,7 @@ Section Transitivity.
       {
         eapply whred_det ; tea.
         - eapply algo_conv_wh in H7 as [] ; gen_typing.
-        - eapply algo_conv_wh in Hconv as [] ; gen_typing. 
+        - eapply algo_conv_wh in Hconv as [] ; gen_typing.
       }
       econstructor ; tea.
       eapply IH ; tea.
@@ -983,7 +984,7 @@ Section Transitivity.
         eapply red_whnf.
         2: gen_typing.
         now eapply red_ty_compl_univ_r, redty_red in Hconvty.
-      }  
+      }
       inversion Hconv ; subst ; clear Hconv ; refold.
       2: now inversion H1.
       now econstructor.
@@ -1070,7 +1071,7 @@ Module AlgorithmicConvProperties.
     - red ; intros_bn.
       eapply algo_conv_sym.
       + now econstructor.
-      + now eapply ctx_refl. 
+      + now eapply ctx_refl.
     - red ; intros * Hconv [? ? ? Hconv'].
       econstructor ; tea.
       1: now apply Hconv.
@@ -1106,7 +1107,7 @@ Module AlgorithmicConvProperties.
         * symmetry.
           now eapply algo_conv_sound in bun_conv_ty0.
       + now do 2 econstructor.
-    - intros * convA. 
+    - intros * convA.
       pose proof convA as ?%bn_conv_sound.
       revert convA; intros_bn.
       + now econstructor.
@@ -1122,7 +1123,7 @@ Qed.
     - red ; intros_bn.
       eapply algo_conv_sym.
       + now econstructor.
-      + now eapply ctx_refl.  
+      + now eapply ctx_refl.
     - red. intros * Hconv [? ? ? Hconv'].
       split ; tea.
       1: apply Hconv.
@@ -1539,7 +1540,7 @@ Module IntermediateTypingProperties.
       + inversion bun_conv_tm ; subst ; clear bun_conv_tm ; refold.
         econstructor.
         4: eassumption.
-        all: now etransitivity. 
+        all: now etransitivity.
     - gen_typing.
     - intros * ? [] [].
       split ; tea.
@@ -1667,7 +1668,7 @@ Module IntermediateTypingProperties.
       + now eapply typing_wk.
       + now eapply credalg_wk.
     - intros * []; assumption.
-    - now intros * []. 
+    - now intros * [].
     - intros; constructor.
       + boundary.
       + econstructor ; tea.
@@ -1710,7 +1711,7 @@ Module IntermediateTypingProperties.
     - intros; econstructor; tea.
       1: boundary.
       1: gen_typing.
-      econstructor. 
+      econstructor.
       2: reflexivity.
       constructor.
     - intros * [].
@@ -1718,12 +1719,12 @@ Module IntermediateTypingProperties.
       1: gen_typing.
       clear -buni_red_tm; induction buni_red_tm.
       1: reflexivity.
-      econstructor; eauto. 
+      econstructor; eauto.
       now constructor.
     - intros; econstructor; tea.
       1: boundary.
       1: gen_typing.
-      econstructor. 
+      econstructor.
       2: reflexivity.
       constructor.
     - intros * [].
@@ -1731,7 +1732,7 @@ Module IntermediateTypingProperties.
       1: gen_typing.
       clear -buni_red_tm; induction buni_red_tm.
       1: reflexivity.
-      econstructor; eauto. 
+      econstructor; eauto.
       now constructor.
     - intros * ??????? convA convxy convxz.
       pose proof convA as ?%bn_conv_sound.
@@ -1745,7 +1746,7 @@ Module IntermediateTypingProperties.
       1: econstructor; tea; now econstructor.
       symmetry; econstructor; tea.
       etransitivity; tea; now symmetry.
-    - intros * ????? []. 
+    - intros * ????? [].
       econstructor; tea.
       2: now eapply redalg_idElim.
       now econstructor.
diff --git a/theories/AutoSubst/Ast.v b/theories/AutoSubst/Ast.v
index 7667d2e..43a9129 100644
--- a/theories/AutoSubst/Ast.v
+++ b/theories/AutoSubst/Ast.v
@@ -204,7 +204,7 @@ Proof.
 exact (scons (tRel var_zero) (funcomp (ren_term shift) sigma)).
 Defined.
 
-Fixpoint subst_term (sigma_term : nat -> term) (s : term) {struct s} : 
+Fixpoint subst_term (sigma_term : nat -> term) (s : term) {struct s} :
 term :=
   match s with
   | tRel s0 => sigma_term s0
@@ -1063,8 +1063,8 @@ Class Up_term X Y :=
 #[global]
 Instance VarInstance_term : (Var _ _) := @tRel.
 
-Notation "[ sigma_term ]" := (subst_term sigma_term)
-  ( at level 1, left associativity, only printing) : fscope.
+(* Notation "[ sigma_term ]" := (subst_term sigma_term)
+  ( at level 1, left associativity, only printing) : fscope. *)
 
 Notation "s [ sigma_term ]" := (subst_term sigma_term s)
   ( at level 7, left associativity, only printing) : subst_scope.
@@ -1132,7 +1132,7 @@ Tactic Notation "auto_unfold" "in" "*" := repeat
                                            unfold VarInstance_term, Var, ids,
                                             Ren_term, Ren1, ren1,
                                             Up_term_term, Up_term, up_term,
-                                            Subst_term, Subst1, subst1 
+                                            Subst_term, Subst1, subst1
                                             in *.
 
 Ltac asimpl' := repeat (first
diff --git a/theories/Decidability/Functions.v b/theories/Decidability/Functions.v
index 4997329..921ffeb 100644
--- a/theories/Decidability/Functions.v
+++ b/theories/Decidability/Functions.v
@@ -138,9 +138,9 @@ Definition build_ty_view1 t : ty_view1 t :=
   | tm_view1_type e => ty_view1_ty e
   | tm_view1_rel n => ty_view1_small (ne_view1_rel n)
   | tm_view1_dest t s => ty_view1_small (ne_view1_dest t s)
-  | tm_view1_fun _ _ 
-  | tm_view1_nat _ 
-  | tm_view1_sig _ _ _ _ 
+  | tm_view1_fun _ _
+  | tm_view1_nat _
+  | tm_view1_sig _ _ _ _
   | tm_view1_id _ _ => ty_view1_anomaly
   end.
 
@@ -161,7 +161,7 @@ Definition callTypesFactory I (F : I -> Type) (f : forall i, F i) (pfuns : foral
 |}.
 
 #[program]
-Definition callablePropsFactory I (F : I -> Type) (f : forall i, F i) (pfuns : forall (i :I), PFun (f i)) 
+Definition callablePropsFactory I (F : I -> Type) (f : forall i, F i) (pfuns : forall (i :I), PFun (f i))
   : CallableProps (callTypesFactory I F f pfuns) := {|
   cp_graph i := pgraph (f i) ;
   cp_fueled i := pfueled (f i) ;
@@ -183,7 +183,7 @@ Next Obligation. intros; now eapply pdef_graph. Qed.
         (fun bot => match bot return False_rect _ bot with end)
         (fun bot => match bot return PFun@{Set Set Set} _ with end).
 
-Equations wh_red_stack : ∇(_ : term × stack), False ⇒ term :=
+Equations wh_red_stack : ∇(_ : term × stack), [False]⇒ term :=
   wh_red_stack (t,π) with (build_tm_view1 t) :=
   wh_red_stack (?(tRel n)       ,π)                           (tm_view1_rel n) := ret (zip (tRel n) π) ;
   wh_red_stack (?(zip1 t s)     ,π)                           (tm_view1_dest t s) := rec (t,cons s π) ;
@@ -243,7 +243,7 @@ Definition call_single {F}
 
 #[export] Instance: PFun wh_red_stack := pfun_gen _ _ wh_red_stack.
 
-Definition wh_red : ∇(t : term), Sing wh_red_stack ⇒ term :=
+Definition wh_red : ∇(t : term), [Sing wh_red_stack]⇒ term :=
   fun t => call_single wh_red_stack (t,nil).
 
 #[export] Instance: PFun wh_red := pfun_gen _ _ wh_red.
@@ -327,7 +327,7 @@ Equations build_nf_view3 T t t' : nf_view3 T t t' :=
   (** Inhabitants of the empty type must be neutrals *)
   | ty_view1_ty eEmpty with (build_nf_view1 t), (build_nf_view1 t') :=
   {
-    | nf_view1_ne _, nf_view1_ne _ := 
+    | nf_view1_ne _, nf_view1_ne _ :=
       neutrals _ _ _ ;
     | _, _ := anomaly _ _ _ ;
   }
@@ -469,7 +469,7 @@ Equations conv_tm_red : conv_stmt tm_red_state :=
     | pairs A B t u :=
         rec (tm_state;Γ;A;tFst t; tFst u) ;;
         rec (tm_state;Γ; B[(tFst t)..]; tSnd t; tSnd u) (* ::: (tm_red_state;Γ;tSig A B;t;u) ;*) ;
-    | refls A x y A' x' A'' x'' := 
+    | refls A x y A' x' A'' x'' :=
       rec (ty_state;Γ;tt;A';A'') ;;
       rec (tm_state;Γ;A';x';x'')
     | neutrals _ _ _ :=
@@ -491,7 +491,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
   {
     | _, _, Some (ne_view1_rel n, ne_view1_rel n') with n =? n' :=
     { | false := raise (variable_mismatch n n') ;
-      | true with (ctx_access Γ n) := 
+      | true with (ctx_access Γ n) :=
         {
         | exception e => undefined ;
         | success d => ret d (* ::: (ne_state;Γ;inp;tRel n; tRel n')*)
@@ -500,7 +500,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
     | _, _, Some (ne_view1_dest n (eApp t), ne_view1_dest n' (eApp t')) =>
       T ← rec (ne_red_state;Γ;tt;n;n') ;;
       match T with
-      | tProd A B => 
+      | tProd A B =>
         rec (tm_state;Γ;A;t;t') ;; ret B[t..]
       |  _ => undefined (** the whnf of the type of an applied neutral must be a Π type!*)
       end ;
@@ -525,7 +525,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
     | _, _, Some (ne_view1_dest n eFst, ne_view1_dest n' eFst) =>
       T ← rec (ne_red_state;Γ;tt;n;n') ;;
       match T with
-      | tSig A B => ret A 
+      | tSig A B => ret A
       | _ => undefined (** the whnf of the type of a projected neutral must be a Σ type!*)
       end ;
     | _, _, Some (ne_view1_dest n eSnd, ne_view1_dest n' eSnd) =>
@@ -533,7 +533,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
       match T with
       | tSig A B => ret B[(tFst n)..]
       | _ => undefined (** the whnf of the type of a projected neutral must be a Σ type!*)
-      end ; 
+      end ;
     | _, _, Some (ne_view1_dest n (eIdElim A x P hr y), ne_view1_dest n' (eIdElim A' x' P' hr' y')) =>
       T ← rec (ne_red_state;Γ;tt;n;n') ;;
       match T with
@@ -554,7 +554,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
   | (Γ;inp;tRel n;tRel n')
     with n =? n' :=
     { | false := raise (variable_mismatch n n') ;
-      | true with (ctx_access Γ n) := 
+      | true with (ctx_access Γ n) :=
         {
         | error e => undefined ;
         | ok d => ret d (* ::: (ne_state;Γ;inp;tRel n; tRel n')*)
@@ -563,7 +563,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
   | (Γ;inp;tApp n t ; tApp n' t') :=
     T ← rec (ne_red_state;Γ;tt;n;n') ;;
     match T with
-    | tProd A B => 
+    | tProd A B =>
       rec (tm_state;Γ;A;t;t') ;; ret B[t..]
       (* (ret (B[t..])) ::: (ne_state;Γ;inp;tApp n t; tApp n' t') *)
     |  _ => undefined (** the whnf of the type of an applied neutral must be a Π type!*)
@@ -600,7 +600,7 @@ Time Equations conv_ne : conv_stmt ne_state :=
     | tSig A B => ret B[(tFst n)..]
       (* ret (B[(tFst n)..]) ::: (ne_state;Γ; inp; tSnd n; tSnd n') *)
     | _ => undefined (** the whnf of the type of a projected neutral must be a Σ type!*)
-    end ; 
+    end ;
   | (Γ;_;n;n') := raise (destructor_mismatch n n'). *)
 
 Equations conv_ne_red : conv_stmt ne_red_state :=
@@ -609,7 +609,8 @@ Equations conv_ne_red : conv_stmt ne_red_state :=
     r ← call_single wh_red Ainf ;;[M0]
     ret (M:=M) r.
 
-Equations conv : ∇(x : conv_full_dom), Sing wh_red ⇒ exn errors ♯ cstate_output x.π1 :=
+
+Equations conv : ∇(x : conv_full_dom), [Sing wh_red]⇒[exn errors] cstate_output x.π1 :=
   | (ty_state; Γ ; inp ; T; V) := conv_ty (Γ; inp; T; V);
   | (ty_red_state; Γ ; inp ; T; V) := conv_ty_red (Γ; inp; T; V);
   | (tm_state; Γ ; inp ; T; V) := conv_tm (Γ; inp; T; V);
@@ -804,7 +805,7 @@ Equations typing_wf_ty : typing_stmt wf_ty_state :=
     T' ← rec (inf_state;Γ;tt;t) ;;[M]
     ext_call (I:=ϕ) (mkRight conv) (ty_state;Γ;tt;T';T).
 
-  Equations typing : ∇ (x : typing_full_dom), ϕ ⇒ exn errors ♯ tstate_output x.π1 :=
+  Equations typing : ∇ (x : typing_full_dom), [ϕ]⇒[exn errors] tstate_output x.π1 :=
   | (wf_ty_state; Γ; inp; T) := typing_wf_ty (Γ;inp;T)
   | (inf_state; Γ; inp; t) := typing_inf (Γ;inp;t)
   | (inf_red_state; Γ; inp; t) := typing_inf_red (Γ;inp;t)
@@ -816,7 +817,7 @@ End Typing.
 
 Section CtxTyping.
 
-  Equations check_ctx : ∇ (Γ : context), Sing typing ⇒ exn errors ♯ unit :=
+  Equations check_ctx : ∇ (Γ : context), [Sing typing]⇒[exn errors] unit :=
     check_ctx ε := ret tt ;
     check_ctx (Γ,,A) :=
       rec Γ ;;[combined_orec (exn _) _ _ _]
diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v
index 5e707c5..f7a0447 100644
--- a/theories/LogicalRelation.v
+++ b/theories/LogicalRelation.v
@@ -62,7 +62,7 @@ Definition LRPackAdequate@{i j} {Γ : context} {A : term}
 Arguments LRPackAdequate _ _ /.
 
 Module LRAd.
-  
+
   Record > LRAdequate@{i j} {Γ : context} {A : term} {R : RedRel@{i j}} : Type :=
   {
     pack :> LRPack@{i} Γ A ;
@@ -212,7 +212,7 @@ Notation "[ Γ ||-U< l > A ]" := (URedTy l Γ A) (at level 0, Γ, l, A at level
 
 Module URedTyEq.
 
-  Record URedTyEq `{ta : tag} `{!WfType ta} `{!RedType ta} 
+  Record URedTyEq `{ta : tag} `{!WfType ta} `{!RedType ta}
     {Γ : context} {B : term} : Set := {
     red : [Γ |- B :⤳*: U]
   }.
@@ -316,7 +316,7 @@ Export PolyRedPack(PolyRedPack, Build_PolyRedPack, PolyRedPackAdequate, Build_Po
 Module PolyRedEq.
 
   Record PolyRedEq `{ta : tag} `{WfContext ta}
-    `{WfType ta} `{ConvType ta} 
+    `{WfType ta} `{ConvType ta}
     {Γ : context} {shp pos: term} {PA : PolyRedPack Γ shp pos} {shp' pos' : term}
   : Type := {
     shpRed {Δ} (ρ : Δ ≤ Γ) (h : [ |- Δ ]) :
@@ -380,7 +380,7 @@ Coercion ParamRedTyEq.polyRed : ParamRedTyEq >-> PolyRedEq.
 
 (** ** Reducibility of product types *)
 
-Definition PiRedTy `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} := 
+Definition PiRedTy `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} :=
   ParamRedTyPack (T:=tProd).
 
 Definition PiRedTyAdequate@{i j} `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
@@ -390,8 +390,8 @@ Definition PiRedTyAdequate@{i j} `{ta : tag} `{WfContext ta} `{WfType ta} `{Conv
 (* keep ? *)
 Module PiRedTy := ParamRedTyPack.
 Notation "[ Γ ||-Πd A ]" := (PiRedTy Γ A).
-  
-Definition PiRedTyEq `{ta : tag} 
+
+Definition PiRedTyEq `{ta : tag}
   `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
   {Γ : context} {A : term} (ΠA : PiRedTy Γ A) (B : term) :=
   ParamRedTyEq (T:=tProd) Γ A B ΠA.
@@ -466,14 +466,14 @@ Notation "[ Γ ||-Π t ≅ u : A | ΠA ]" := (PiRedTmEq Γ t u A ΠA).
 
 (** ** Reducibility of dependent sum types *)
 
-Definition SigRedTy `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} := 
+Definition SigRedTy `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta} :=
   ParamRedTyPack (T:=tSig).
 
 Definition SigRedTyAdequate@{i j} `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
     {Γ : context} {A : term} (R : RedRel@{i j}) (ΣA : SigRedTy@{i} Γ A)
   : Type@{j} := PolyRedPackAdequate R ΣA.
-  
-Definition SigRedTyEq `{ta : tag} 
+
+Definition SigRedTyEq `{ta : tag}
   `{WfContext ta} `{WfType ta} `{ConvType ta} `{RedType ta}
   {Γ : context} {A : term} (ΠA : SigRedTy Γ A) (B : term) :=
   ParamRedTyEq (T:=tSig) Γ A B ΠA.
@@ -574,7 +574,7 @@ Module NatRedTy.
 
   Record NatRedTy `{ta : tag} `{WfType ta} `{RedType ta}
     {Γ : context} {A : term}
-  : Set := 
+  : Set :=
   {
     red : [Γ |- A :⤳*: tNat]
   }.
@@ -603,7 +603,7 @@ Notation "[ Γ ||-Nat A ≅ B | RA ]" := (@NatRedTyEq _ _ _ Γ A RA B) (at level
 
 Module NatRedTm.
 Section NatRedTm.
-  Context `{ta : tag} `{WfType ta} 
+  Context `{ta : tag} `{WfType ta}
     `{RedType ta} `{Typing ta} `{ConvNeuConv ta} `{ConvTerm ta}
     `{RedTerm ta}.
 
@@ -733,7 +733,7 @@ Module EmptyRedTy.
 
   Record EmptyRedTy `{ta : tag} `{WfType ta} `{RedType ta}
     {Γ : context} {A : term}
-  : Set := 
+  : Set :=
   {
     red : [Γ |- A :⤳*: tEmpty]
   }.
@@ -762,7 +762,7 @@ Notation "[ Γ ||-Empty A ≅ B | RA ]" := (@EmptyRedTyEq _ _ _ Γ A RA B) (at l
 
 Module EmptyRedTm.
 Section EmptyRedTm.
-  Context `{ta : tag} `{WfType ta} 
+  Context `{ta : tag} `{WfType ta}
     `{RedType ta} `{Typing ta} `{ConvNeuConv ta} `{ConvTerm ta}
     `{RedTerm ta}.
 
@@ -827,10 +827,10 @@ Notation "[ Γ ||-Empty t ≅ u : A | RA ]" := (@EmptyRedTmEq _ _ _ _ _ _ _ Γ A
 (** ** Logical relation for Identity types *)
 
 Module IdRedTyPack.
-  
+
   Record IdRedTyPack@{i} `{ta : tag} `{WfContext ta} `{WfType ta} `{RedType ta} `{ConvType ta}
     {Γ : context} {A : term}
-  : Type := 
+  : Type :=
   {
     ty : term ;
     lhs : term ;
@@ -855,7 +855,7 @@ Module IdRedTyPack.
   }.
 
   Record IdRedTyAdequate@{i j} `{ta : tag} `{WfContext ta} `{WfType ta} `{RedType ta} `{ConvType ta}
-    {Γ : context} {A : term} {R : RedRel@{i j}} {IA : IdRedTyPack@{i} (Γ:=Γ) (A:=A)} := 
+    {Γ : context} {A : term} {R : RedRel@{i j}} {IA : IdRedTyPack@{i} (Γ:=Γ) (A:=A)} :=
     {
       tyAd : LRPackAdequate@{i j} R IA.(tyRed) ;
       tyKripkeAd : forall {Δ} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), LRPackAdequate@{i j} R (IA.(tyKripke) ρ wfΔ) ;
@@ -863,7 +863,7 @@ Module IdRedTyPack.
 
   Arguments IdRedTyPack {_ _ _ _ _}.
   Arguments IdRedTyAdequate {_ _ _ _ _ _ _}.
-  
+
 End IdRedTyPack.
 
 Export IdRedTyPack(IdRedTyPack, Build_IdRedTyPack, IdRedTyAdequate, Build_IdRedTyAdequate).
@@ -887,7 +887,7 @@ Module IdRedTyEq.
     lhsRed : [ tyRed0 | _ ||- IA.(IdRedTyPack.lhs) ≅ lhs : _ ] ;
     rhsRed : [ tyRed0 | _ ||- IA.(IdRedTyPack.rhs) ≅ rhs : _ ] ;
   }.
-  
+
   Arguments IdRedTyEq {_ _ _ _ _ _ _ _}.
 
 End IdRedTyEq.
@@ -897,12 +897,12 @@ Export IdRedTyEq(IdRedTyEq,Build_IdRedTyEq).
 Module IdRedTm.
 Section IdRedTm.
   Universe i.
-  Context `{ta : tag} `{WfContext ta} `{WfType ta} 
+  Context `{ta : tag} `{WfContext ta} `{WfType ta}
     `{RedType ta} `{Typing ta} `{ConvType ta} `{ConvNeuConv ta} `{ConvTerm ta}
     `{RedTerm ta} {Γ : context} {A: term} {IA : IdRedTyPack@{i} Γ A}.
 
   Inductive IdProp : term ->  Type:=
-  | reflR {A x} : 
+  | reflR {A x} :
     [Γ |- A] ->
     [Γ |- x : A] ->
     [IA.(IdRedTyPack.tyRed) | _ ||- _ ≅ A] ->
@@ -918,7 +918,7 @@ Section IdRedTm.
       red : [Γ |- t :⤳*: nf : IA.(IdRedTyPack.outTy) ] ;
       eq : [Γ |- nf ≅ nf : IA.(IdRedTyPack.outTy)] ;
       prop : IdProp nf ;
-  }. 
+  }.
 
 End IdRedTm.
 Arguments IdRedTm {_ _ _ _ _ _ _ _ _ _ _}.
@@ -935,17 +935,17 @@ Section IdRedTmEq.
   Context `{ta : tag} `{WfContext ta} `{WfType ta} `{ConvType ta}
     `{RedType ta} `{Typing ta} `{ConvNeuConv ta} `{ConvTerm ta}
     `{RedTerm ta} {Γ : context} {A: term} {IA : IdRedTyPack@{i} Γ A}.
-  
+
   Inductive IdPropEq : term -> term -> Type :=
-  | reflReq {A A' x x'} : 
+  | reflReq {A A' x x'} :
     [Γ |- A] ->
     [Γ |- A'] ->
     [Γ |- x : A] ->
     [Γ |- x' : A'] ->
     [IA.(IdRedTyPack.tyRed) | _ ||- _ ≅ A] ->
     [IA.(IdRedTyPack.tyRed) | _ ||- _ ≅ A'] ->
-    [IA.(IdRedTyPack.tyRed) | _ ||- IA.(IdRedTyPack.lhs) ≅ x : _ ] -> 
-    [IA.(IdRedTyPack.tyRed) | _ ||- IA.(IdRedTyPack.lhs) ≅ x' : _ ] -> 
+    [IA.(IdRedTyPack.tyRed) | _ ||- IA.(IdRedTyPack.lhs) ≅ x : _ ] ->
+    [IA.(IdRedTyPack.tyRed) | _ ||- IA.(IdRedTyPack.lhs) ≅ x' : _ ] ->
     (* Should the indices only be conversion ? *)
     [IA.(IdRedTyPack.tyRed) | _ ||- IA.(IdRedTyPack.rhs) ≅ x : _ ] ->
     [IA.(IdRedTyPack.tyRed) | _ ||- IA.(IdRedTyPack.rhs) ≅ x' : _ ] ->
@@ -960,7 +960,7 @@ Section IdRedTmEq.
       redR : [Γ |- u :⤳*: nfR : IA.(IdRedTyPack.outTy) ] ;
       eq : [Γ |- nfL ≅ nfR : IA.(IdRedTyPack.outTy)] ;
       prop : IdPropEq nfL nfR ;
-  }. 
+  }.
 
 End IdRedTmEq.
 Arguments IdRedTmEq {_ _ _ _ _ _ _ _ _ _ _}.
@@ -1006,7 +1006,7 @@ Inductive LR@{i j k} `{ta : tag}
   | LRId {Γ A} (IA : IdRedTyPack@{j} Γ A) (IAad : IdRedTyAdequate@{j k} (LR rec) IA) :
     LR rec Γ A (IdRedTyEq IA) (IdRedTm IA) (IdRedTmEq IA)
   .
-  
+
   (** Removed, as it is provable (!), cf LR_embedding in LRInduction. *)
   (* | LREmb {Γ A l'} (l_ : l' << l) (H : [ rec l' l_ | Γ ||- A]) :
       LR rec Γ A
@@ -1080,21 +1080,21 @@ Section MoreDefs.
     : [ LogRel@{i j k l} l | Γ ||- A ] :=
     LRbuild (LRPi (LogRelRec l) ΠA ΠAad).
 
-  Definition LRNat_@{i j k l} l {Γ A} (NA : [Γ ||-Nat A]) 
+  Definition LRNat_@{i j k l} l {Γ A} (NA : [Γ ||-Nat A])
     : [LogRel@{i j k l} l | Γ ||- A] :=
     LRbuild (LRNat (LogRelRec l) NA).
 
-  Definition LREmpty_@{i j k l} l {Γ A} (NA : [Γ ||-Empty A]) 
+  Definition LREmpty_@{i j k l} l {Γ A} (NA : [Γ ||-Empty A])
     : [LogRel@{i j k l} l | Γ ||- A] :=
     LRbuild (LREmpty (LogRelRec l) NA).
 
-  Definition LRId_@{i j k l} l {Γ A} (IA : IdRedTyPack@{k} Γ A) 
+  Definition LRId_@{i j k l} l {Γ A} (IA : IdRedTyPack@{k} Γ A)
     (IAad : IdRedTyAdequate (LR (LogRelRec@{i j k} l)) IA)
     : [LogRel@{i j k l} l | Γ ||- A] :=
     LRbuild (LRId (LogRelRec l) IA IAad).
 
 End MoreDefs.
-  
+
 (** To be explicit with universe levels use the rhs, e.g
    [ LogRel@{i j k l} l | Γ ||- A] or [ LogRel0@{i j k} ||- Γ ||- A ≅ B | RA ]
  *)
@@ -1140,8 +1140,8 @@ Section PolyRed.
         [ (shpRed ρ h) | Δ ||- a ≅ b : shp⟨ρ⟩] ->
         [ (posRed ρ h ha) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]
     }.
-  
-  Definition from@{i j k l} {PA : PolyRedPack@{k} Γ shp pos} 
+
+  Definition from@{i j k l} {PA : PolyRedPack@{k} Γ shp pos}
     (PAad : PolyRedPackAdequate@{k l} (LogRel@{i j k l} l) PA)
     : PolyRed@{i j k l}.
   Proof.
@@ -1152,16 +1152,16 @@ Section PolyRed.
     - now eapply PolyRedPack.posTy.
     - now eapply PolyRedPack.posExt.
   Defined.
-  
+
   Definition toPack@{i j k l} (PA : PolyRed@{i j k l}) : PolyRedPack@{k} Γ shp pos.
   Proof.
     unshelve econstructor.
     - now eapply shpRed.
     - intros; now eapply posRed.
-    - now eapply shpTy. 
+    - now eapply shpTy.
     - now eapply posTy.
     - intros; now eapply posExt.
-  Defined. 
+  Defined.
 
   Definition toAd@{i j k l} (PA : PolyRed@{i j k l}) : PolyRedPackAdequate@{k l} (LogRel@{i j k l} l) (toPack PA).
   Proof.
@@ -1173,12 +1173,12 @@ Section PolyRed.
   Lemma eta@{i j k l} (PA : PolyRed@{i j k l}) : from (toAd PA) = PA.
   Proof. destruct PA; reflexivity. Qed.
 
-  Lemma beta_pack@{i j k l} {PA : PolyRedPack@{k} Γ shp pos} 
+  Lemma beta_pack@{i j k l} {PA : PolyRedPack@{k} Γ shp pos}
     (PAad : PolyRedPackAdequate@{k l} (LogRel@{i j k l} l) PA)
     : toPack (from PAad) = PA.
   Proof. destruct PA, PAad; reflexivity. Qed.
 
-  Lemma beta_ad@{i j k l} {PA : PolyRedPack@{k} Γ shp pos} 
+  Lemma beta_ad@{i j k l} {PA : PolyRedPack@{k} Γ shp pos}
     (PAad : PolyRedPackAdequate@{k l} (LogRel@{i j k l} l) PA)
     : toAd (from PAad) = PAad.
   Proof. destruct PA, PAad; reflexivity. Qed.
@@ -1224,7 +1224,7 @@ Section ParamRedTy.
   Defined.
 
   Definition toPack@{i j k l} (PA : ParamRedTy@{i j k l}) :
-    ParamRedTyPack@{k} (T:=T) Γ A. 
+    ParamRedTyPack@{k} (T:=T) Γ A.
   Proof.
     exists (dom PA) (cod PA).
     - now eapply red.
@@ -1233,7 +1233,7 @@ Section ParamRedTy.
     - exact (PolyRed.toPack PA).
   Defined.
 
-  Definition toAd@{i j k l} (PA : ParamRedTy@{i j k l}) :  
+  Definition toAd@{i j k l} (PA : ParamRedTy@{i j k l}) :
     PolyRedPackAdequate@{k l} (LogRel@{i j k l} l) (toPack PA) :=
     PolyRed.toAd PA.
 
@@ -1245,7 +1245,7 @@ Section ParamRedTy.
     : toPack (from PAad) = PA.
   Proof. destruct PA, PAad; reflexivity. Qed.
 
-  Lemma beta_ad@{i j k l} {PA : ParamRedTyPack@{k} (T:=T) Γ A} 
+  Lemma beta_ad@{i j k l} {PA : ParamRedTyPack@{k} (T:=T) Γ A}
     (PAad : PolyRedPackAdequate@{k l} (LogRel@{i j k l} l) PA)
     : toAd (from PAad) = PAad.
   Proof. destruct PA, PAad; reflexivity. Qed.
@@ -1270,7 +1270,7 @@ Section EvenMoreDefs.
     `{!WfContext ta} `{!WfType ta} `{!Typing ta}
     `{!ConvType ta} `{!ConvTerm ta} `{!ConvNeuConv ta}
     `{!RedType ta} `{!RedTerm ta}.
-  
+
   Definition LRPi'@{i j k l} {l Γ A} (ΠA : ParamRedTy@{i j k l} tProd Γ l A)
     : [ LogRel@{i j k l} l | Γ ||- A ] :=
     LRbuild (LRPi (LogRelRec l) _ (ParamRedTy.toAd ΠA)).
@@ -1290,22 +1290,25 @@ Section LogRelRecFoldLemmas.
     `{!ConvType ta} `{!ConvTerm ta} `{!ConvNeuConv ta}
     `{!RedType ta} `{!RedTerm ta}.
 
-  Lemma RedTyRecFwd {l Γ A t} (h : [Γ ||-U<l> A]) : 
-    [LogRelRec l (URedTy.level h) (URedTy.lt h) | Γ ||- t] ->
-    [LogRel (URedTy.level h) | Γ ||- t ].
+  Lemma RedTyRecFwd@{i j k l} {l Γ A t} (h : [Γ ||-U<l> A]) :
+    [LogRelRec@{j k l} l (URedTy.level h) (URedTy.lt h) | Γ ||- t] ->
+    [LogRel@{i j k l} (URedTy.level h) | Γ ||- t ].
   Proof.
-    destruct h as [? lt]; cbn. 
-    pattern level, l , lt; induction lt.
-    cbn. easy. 
+    destruct h as [? lt]; cbn.
+    pattern level, l , lt.
+    (* Employ using to specify the universe level l instead of generating a fresh one *)
+    induction lt using TypeLevelLt_rect@{l}.
+    cbn. easy.
   Defined.
 
-  Lemma RedTyRecBwd {l Γ A t} (h : [Γ ||-U<l> A]) : 
-    [LogRel (URedTy.level h) | Γ ||- t ] ->
-    [LogRelRec l (URedTy.level h) (URedTy.lt h) | Γ ||- t].
+  Lemma RedTyRecBwd@{i j k l} {l Γ A t} (h : [Γ ||-U<l> A]) :
+    [LogRel@{i j k l} (URedTy.level h) | Γ ||- t ] ->
+    [LogRelRec@{j k l} l (URedTy.level h) (URedTy.lt h) | Γ ||- t].
   Proof.
     destruct h as [? lt]; cbn.
-    pattern level, l , lt; induction lt.
-    cbn. easy. 
+    (* Employ using to specify the universe level l instead of generating a fresh one *)
+    pattern level, l , lt; induction lt using TypeLevelLt_rect@{l}.
+    cbn. easy.
   Defined.
 
   (* This is a duplicate of the above, no ? *)
@@ -1318,7 +1321,7 @@ Section LogRelRecFoldLemmas.
   Qed.
 
 
-  Lemma TyEqRecFwd {l Γ A t u} (h : [Γ ||-U<l> A]) 
+  Lemma TyEqRecFwd {l Γ A t u} (h : [Γ ||-U<l> A])
     (lr : [LogRelRec l (URedTy.level h) (URedTy.lt h) | Γ ||- t]) :
     [lr | Γ ||- t ≅ u] <~> [RedTyRecFwd h lr | Γ ||- t ≅ u].
   Proof.
@@ -1327,7 +1330,7 @@ Section LogRelRecFoldLemmas.
     induction lt; cbn; split; easy.
   Qed.
 
-  Lemma TyEqRecBwd {l Γ A t u} (h : [Γ ||-U<l> A]) 
+  Lemma TyEqRecBwd {l Γ A t u} (h : [Γ ||-U<l> A])
     (lr : [LogRel (URedTy.level h) | Γ ||- t ]) :
     [lr | Γ ||- t ≅ u] <~> [RedTyRecBwd h lr | Γ ||- t ≅ u].
   Proof.
@@ -1365,7 +1368,7 @@ End EmptyPropProperties.
 
 Lemma EmptyRedInduction :
   forall {ta : tag} {H : WfType ta} {H0 : RedType ta} {H1 : Typing ta}
-    {H2 : ConvNeuConv ta} {H3 : ConvTerm ta} {H4 : RedTerm ta} 
+    {H2 : ConvNeuConv ta} {H3 : ConvTerm ta} {H4 : RedTerm ta}
     (Γ : context) (A : term) (NA : [Γ ||-Empty A])
     (P : forall t : term, [Γ ||-Empty t : A | NA] -> Type)
     (P0 : forall t : term, EmptyProp Γ t -> Type),
@@ -1385,7 +1388,7 @@ Qed.
 
 Lemma EmptyRedEqInduction :
   forall {ta : tag} {H0 : WfType ta} {H2 : RedType ta} {H3 : Typing ta}
-    {H4 : ConvNeuConv ta} {H5 : ConvTerm ta} {H6 : RedTerm ta} 
+    {H4 : ConvNeuConv ta} {H5 : ConvTerm ta} {H6 : RedTerm ta}
     (Γ : context) (A : term) (NA : [Γ ||-Empty A])
     (P : forall t t0 : term, [Γ ||-Empty t ≅ t0 : A | NA] -> Type)
     (P0 : forall t t0 : term, EmptyPropEq Γ t t0 -> Type),
@@ -1407,13 +1410,13 @@ Qed.
 
 Module IdRedTy.
 Section IdRedTy.
-  
+
   Context `{ta : tag}
     `{!WfContext ta} `{!WfType ta} `{!Typing ta}
     `{!ConvType ta} `{!ConvTerm ta} `{!ConvNeuConv ta}
     `{!RedType ta} `{!RedTerm ta}.
 
-  Record IdRedTy@{i j k l} {Γ : context} {l} {A : term} : Type := 
+  Record IdRedTy@{i j k l} {Γ : context} {l} {A : term} : Type :=
   {
     ty : term ;
     lhs : term ;
@@ -1437,7 +1440,7 @@ Section IdRedTy.
  }.
 
 
-  Definition from@{i j k l} {Γ l A} {IA : IdRedTyPack@{k} Γ A} (IAad : IdRedTyAdequate@{k l} (LogRel@{i j k l} l) IA) 
+  Definition from@{i j k l} {Γ l A} {IA : IdRedTyPack@{k} Γ A} (IAad : IdRedTyAdequate@{k l} (LogRel@{i j k l} l) IA)
     : @IdRedTy@{i j k l} Γ l A.
   Proof.
     unshelve econstructor; try exact IA.(IdRedTyPack.red).
@@ -1455,7 +1458,7 @@ Section IdRedTy.
   Defined.
 
   Definition toPack@{i j k l} {Γ l A} (IA : @IdRedTy@{i j k l} Γ l A) : IdRedTyPack@{k} Γ A.
-  Proof. 
+  Proof.
     unshelve econstructor; try exact IA.(IdRedTy.red).
     - apply IA.(tyRed).
     - intros; now apply IA.(tyKripke).
@@ -1469,21 +1472,21 @@ Section IdRedTy.
     - intros; now eapply IA.(IdRedTy.tyKripkeTm).
     - intros; now eapply IA.(IdRedTy.tyKripkeTmEq).
   Defined.
-  
+
   Definition to@{i j k l} {Γ l A} (IA : @IdRedTy@{i j k l} Γ l A) : IdRedTyAdequate@{k l} (LogRel@{i j k l} l) (toPack IA).
-  Proof. 
-    econstructor; [apply IA.(tyRed)| intros; now apply IA.(tyKripke)]. 
+  Proof.
+    econstructor; [apply IA.(tyRed)| intros; now apply IA.(tyKripke)].
   Defined.
 
   Lemma beta_pack@{i j k l} {Γ l A} {IA : IdRedTyPack@{k} Γ A} (IAad : IdRedTyAdequate@{k l} (LogRel@{i j k l} l) IA) :
     toPack (from IAad) = IA.
   Proof. reflexivity. Qed.
-  
+
   Lemma beta_ad@{i j k l} {Γ l A} {IA : IdRedTyPack@{k} Γ A} (IAad : IdRedTyAdequate@{k l} (LogRel@{i j k l} l) IA) :
     to (from IAad) = IAad.
   Proof. reflexivity. Qed.
 
-  Lemma eta@{i j k l} {Γ l A} (IA : @IdRedTy@{i j k l} Γ l A) : from  (to IA) = IA. 
+  Lemma eta@{i j k l} {Γ l A} (IA : @IdRedTy@{i j k l} Γ l A) : from  (to IA) = IA.
   Proof. reflexivity. Qed.
 
   Definition IdRedTyEq {Γ l A} (IA : @IdRedTy Γ l A) := IdRedTyEq (toPack IA).
@@ -1502,7 +1505,7 @@ End IdRedTy.
 
 Export IdRedTy(IdRedTy, Build_IdRedTy,IdRedTyEq,IdRedTm,IdProp,IdRedTmEq,IdPropEq,LRId').
 
-Ltac unfold_id_outTy := 
+Ltac unfold_id_outTy :=
   change (IdRedTyPack.outTy (IdRedTy.toPack ?IA)) with (tId IA.(IdRedTy.ty) IA.(IdRedTy.lhs) IA.(IdRedTy.rhs)) in *.
 
 Notation "[ Γ ||-Id< l > A ]" := (IdRedTy Γ l A) (at level 0, Γ, l,  A at level 50).
diff --git a/theories/LogicalRelation/Reflexivity.v b/theories/LogicalRelation/Reflexivity.v
index e7541af..ae6c6ae 100644
--- a/theories/LogicalRelation/Reflexivity.v
+++ b/theories/LogicalRelation/Reflexivity.v
@@ -22,7 +22,7 @@ Section Reflexivities.
   Corollary LRTyEqRefl {l Γ A eqTy redTm eqTm}
     (lr : LogRel l Γ A eqTy redTm eqTm) : eqTy A.
   Proof.
-    pose (R := Build_LRPack Γ A eqTy redTm eqTm). 
+    pose (R := Build_LRPack Γ A eqTy redTm eqTm).
     pose (Rad := Build_LRAdequate (pack:=R) lr).
     change [Rad | _ ||- _ ≅ A ]; now eapply reflLRTyEq.
   Qed.
@@ -70,7 +70,7 @@ Section Reflexivities.
       [ Γ ||-<l> t ≅ t : A | lr ].
   Proof.
     pattern l, Γ, A, lr; eapply LR_rect_TyUr; clear l Γ A lr; intros l Γ A.
-    - intros h t [? ? ? ? Rt%RedTyRecFwd@{j k h i k}] ; cbn in *.
+    - intros h t [? ? ? ? Rt%RedTyRecFwd@{h i j k}] ; cbn in *.
       (* Need an additional universe level h < i *)
       Unset Printing Notations.
       pose proof (reflLRTyEq@{h i k j} Rt).
@@ -95,14 +95,15 @@ Section Reflexivities.
       all: cbn; now eauto.
     - intros; now eapply reflIdRedTmEq.
   Qed.
-  
+
   (* Deprecated *)
   Corollary LRTmEqRefl@{h i j k l} {l Γ A eqTy redTm eqTm} (lr : LogRel@{i j k l} l Γ A eqTy redTm eqTm) :
     forall t, redTm t -> eqTm t t.
   Proof.
-    pose (R := Build_LRPack Γ A eqTy redTm eqTm). 
+    pose (R := Build_LRPack Γ A eqTy redTm eqTm).
     pose (Rad := Build_LRAdequate (pack:=R) lr).
     intros t ?; change [Rad | _ ||- t ≅ t : _ ]; now eapply reflLRTmEq.
   Qed.
 
 End Reflexivities.
+
diff --git a/theories/Positivity.v b/theories/Positivity.v
index 2a44b5c..8aa8938 100644
--- a/theories/Positivity.v
+++ b/theories/Positivity.v
@@ -1,3 +1,4 @@
+Unset Automatic Proposition Inductives.
 Record Foo (x : Type -> Type) : Type := {}.
 
 Fail Inductive Bar : Type -> Type :=