True last one (#105)

* Add one missing obvious opt * Optimize presup a bit more
Beluga-lang · Jun 7, 2024 · 8d4598e · 8d4598e
1 parent 276eb8a
commit 8d4598e
Show file tree

Hide file tree

Showing 6 changed files with 82 additions and 66 deletions.
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
@@ -80,8 +80,8 @@ Proof with intuition.
   destruct_by_head per_univ.
   apply -> per_univ_elem_morphism_iff; eauto.
   split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
-  eapply H5.
-  mauto.
+  exvar (relation domain) ltac:(fun R => assert (rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} R) by mauto).
+  intuition.
 Qed.
 
 Lemma rel_exp_pi_cong : forall {i Γ A A' B B'},
@@ -137,10 +137,7 @@ Proof with mautosolve.
   econstructor; mauto.
   eexists.
   per_univ_elem_econstructor; eauto.
-  - intros.
-    eapply rel_exp_pi_core; eauto; try reflexivity.
-    clear dependent c.
-    clear dependent c'.
+  - eapply rel_exp_pi_core; eauto; try reflexivity.
     intros.
     extract_output_info_with o c o' c' env_relΔA...
   - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
@@ -168,7 +165,7 @@ Proof with mautosolve.
   destruct_by_head per_univ.
   functional_eval_rewrite_clear.
   do 2 eexists.
-  repeat split; only 1,3: econstructor; only 3: eapply per_univ_elem_cumu_max_left; mauto; revgoals.
+  repeat split; [econstructor; [| | eapply per_univ_elem_cumu_max_left] | | econstructor]; mauto.
   - eapply rel_exp_pi_core; eauto; try reflexivity.
     intros.
     extract_output_info_with p c p' c' env_relΓA.
@@ -204,18 +201,16 @@ Proof with mautosolve.
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
   eexists.
   split; econstructor; mauto 4.
-  - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | |]; eauto.
-    + intros.
-      eapply rel_exp_pi_core; eauto; try reflexivity.
-      clear dependent c.
-      clear dependent c'.
-      intros.
-      extract_output_info_with o c o' c' env_relΔA.
-      econstructor; eauto.
-      eexists.
-      eapply per_univ_elem_cumu_max_right...
-    + (* `reflexivity` does not work as it uses a "wrong" instance. *)
-      apply Equivalence_Reflexive.
+  - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | | apply Equivalence_Reflexive]; eauto.
+    intros.
+    eapply rel_exp_pi_core; eauto; try reflexivity.
+    clear dependent c.
+    clear dependent c'.
+    intros.
+    extract_output_info_with o c o' c' env_relΔA.
+    econstructor; eauto.
+    eexists.
+    eapply per_univ_elem_cumu_max_right...
   - intros ? **.
     extract_output_info_with o c o' c' env_relΔA.
     econstructor; mauto.

diff --git a/theories/Core/Semantic/Evaluation/Lemmas.v b/theories/Core/Semantic/Evaluation/Lemmas.v
@@ -65,12 +65,12 @@ Ltac functional_eval_rewrite_clear1 :=
   let tactic_error o1 o2 := fail 3 "functional_eval equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
-      clean replace m2 with m1 by first [solve [mauto] | tactic_error m2 m1]; clear H2
+      clean replace m2 with m1 by first [solve [mauto 2] | tactic_error m2 m1]; clear H2
   | H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
-      clean replace r2 with r1 by first [solve [mauto] | tactic_error r2 r1]; clear H2
+      clean replace r2 with r1 by first [solve [mauto 2] | tactic_error r2 r1]; clear H2
   | H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
-      clean replace r2 with r1 by first [solve [mauto] | tactic_error r2 r1]; clear H2
+      clean replace r2 with r1 by first [solve [mauto 2] | tactic_error r2 r1]; clear H2
   | H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
-      clean replace p2 with p1 by first [solve [mauto] | tactic_error p2 p1]; clear H2
+      clean replace p2 with p1 by first [solve [mauto 2] | tactic_error p2 p1]; clear H2
   end.
 Ltac functional_eval_rewrite_clear := repeat functional_eval_rewrite_clear1.
diff --git a/theories/Core/Semantic/NbE.v b/theories/Core/Semantic/NbE.v
@@ -34,7 +34,7 @@ Ltac functional_initial_env_rewrite_clear1 :=
   let tactic_error o1 o2 := fail 3 "functional_initial_env equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : initial_env ?G ?p, H2 : initial_env ?G ?p' |- _ =>
-      clean replace p' with p by first [solve [mauto] | tactic_error p' p]; clear H2
+      clean replace p' with p by first [solve [mauto 2] | tactic_error p' p]; clear H2
   end.
 Ltac functional_initial_env_rewrite_clear := repeat functional_initial_env_rewrite_clear1.
 
@@ -69,6 +69,6 @@ Ltac functional_nbe_rewrite_clear1 :=
   let tactic_error o1 o2 := fail 3 "functional_nbe equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : nbe ?G ?M ?A ?W, H2 : nbe ?G ?M ?A ?W' |- _ =>
-      clean replace W' with W by first [solve [mauto] | tactic_error W' W]; clear H2
+      clean replace W' with W by first [solve [mauto 2] | tactic_error W' W]; clear H2
   end.
 Ltac functional_nbe_rewrite_clear := repeat functional_nbe_rewrite_clear1.
diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
@@ -8,9 +8,10 @@ Ltac destruct_rel_by_assumption in_rel H :=
   repeat
     match goal with
     | H' : {{ Dom ~?c ≈ ~?c' ∈ ?in_rel0 }} |- _ =>
-        tryif (unify in_rel0 in_rel)
-        then (destruct (H _ _ H') as []; destruct_all; mark_with H' 1)
-        else fail
+        unify in_rel0 in_rel;
+        destruct (H _ _ H') as [];
+        destruct_all;
+        mark_with H' 1
     end;
   unmark_all_with 1.
 Ltac destruct_rel_mod_eval :=

diff --git a/theories/Core/Semantic/Readback/Lemmas.v b/theories/Core/Semantic/Readback/Lemmas.v
@@ -52,10 +52,10 @@ Ltac functional_read_rewrite_clear1 :=
   let tactic_error o1 o2 := fail 3 "functional_read equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : {{ Rnf ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rnf ~?m in ?s ↘ ~?M2 }} |- _ =>
-      clean replace M2 with M1 by first [solve [mauto] | tactic_error M2 M1]; clear H2
+      clean replace M2 with M1 by first [solve [mauto 2] | tactic_error M2 M1]; clear H2
   | H1 : {{ Rne ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rne ~?m in ?s ↘ ~?M2 }} |- _ =>
-      clean replace M2 with M1 by first [solve [mauto] | tactic_error M2 M1]; clear H2
+      clean replace M2 with M1 by first [solve [mauto 2] | tactic_error M2 M1]; clear H2
   | H1 : {{ Rtyp ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rtyp ~?m in ?s ↘ ~?M2 }} |- _ =>
-      clean replace M2 with M1 by first [solve [mauto] | tactic_error M2 M1]; clear H2
+      clean replace M2 with M1 by first [solve [mauto 2] | tactic_error M2 M1]; clear H2
   end.
 Ltac functional_read_rewrite_clear := repeat functional_read_rewrite_clear1.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
@@ -80,16 +80,19 @@ Proof with mautosolve 4.
     assert {{ Γ ⊢ B[q σ∘(Id,,N[σ])] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
     assert {{ Γ ⊢ B[q σ][Id,,N[σ]] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
     assert {{ Γ ⊢ NZ[σ] : B[Id ,, zero][σ] }} by mauto.
-    assert {{ Γ ⊢ zero : ℕ[σ] }} by mautosolve.
+    assert {{ Γ ⊢ ℕ ≈ ℕ[σ] : Type@0 }} by mauto.
+    assert {{ Γ ⊢ zero : ℕ[σ] }} by mauto.
     assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto.
     assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto.
     assert {{ Γ ⊢s σ ,, zero ≈ Id∘σ ,, zero[σ] : Δ, ℕ }} by mauto 4.
     assert {{ Γ ⊢s Id∘σ ,, zero[σ] ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢s Id ,, zero : Γ, ℕ }} by mauto.
     assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
-    assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto 4.
+    assert {{ Γ ⊢ B[q σ∘(Id ,, zero)] ≈ B[(Id ,, zero)∘σ] : Type@i }} by mauto.
+    assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto.
     assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto.
     set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
-    assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto.
+    assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto 4.
     assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
     assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
     assert {{ Γ' ⊢ B[q σ][WkWksucc] ≈ B[WkWksucc][q (q σ)] : Type@i }} by mauto.
@@ -101,19 +104,24 @@ Proof with mautosolve 4.
     set (IdNrecN := {{{ Id ,, N ,, recN }}}).
     assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto.
     assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] : Γ, ℕ }}
-      by (eapply sub_eq_extend_compose_nat; mauto).
-    assert {{ Γ ⊢s Id ,, N ,, recN : Γ, ℕ, B }} by mauto.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN : Γ }} by mauto.
+      by (eapply sub_eq_extend_compose_nat; mauto 4).
+    assert {{ Γ ⊢s IdNrecN : Γ, ℕ, B }} by mauto.
+    assert {{ Γ, ℕ, B ⊢s Wk∘Wk : Γ }} by mauto 4.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN : Γ }} by mauto 4.
     assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Wk∘(Wk∘IdNrecN) : Γ }} by mauto 4.
-    assert {{ Γ ⊢s Wk∘(Wk∘IdNrecN) ≈ Wk∘(Id ,, N) : Γ }} by mauto.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Id : Γ }} by mauto.
-    assert {{ Γ ⊢ #1[Id ,, N ,, recN] ≈ #0[Id ,, N] : ℕ }} by mauto.
-    assert {{ Γ ⊢ succ #1[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
-    assert {{ Γ ⊢ (succ #1)[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ,, (succ #1)[Id ,, N ,, recN] ≈ Id ,, succ N : Γ , ℕ }} by mauto.
+    assert {{ Γ ⊢s Id,,N : Γ, ℕ }} by mauto 4.
+    assert {{ Γ ⊢s Wk∘(Wk∘IdNrecN) ≈ Wk∘(Id ,, N) : Γ }} by mauto 4.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Id : Γ }} by mauto 4.
+    assert {{ Γ ⊢ #1[IdNrecN] ≈ #0[Id ,, N] : ℕ }} by mauto.
+    assert {{ Γ ⊢ #1[IdNrecN] ≈ N : ℕ }} by mauto 4.
+    assert {{ Γ ⊢ succ #1[IdNrecN] ≈ succ N : ℕ }} by mauto.
+    assert {{ Γ ⊢ (succ #1)[IdNrecN] ≈ succ N : ℕ }} by mauto 4.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] ≈ Id ,, succ N : Γ , ℕ }} by mauto.
+    assert {{ Γ ⊢s WkWksucc∘IdNrecN : Γ, ℕ }} by mauto.
+    assert {{ Γ ⊢s Id,,succ N : Γ, ℕ }} by mauto.
     assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ Id ,, succ N : Γ , ℕ }} by mauto.
-    assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id ,, succ N] : Type@i }} by mauto 4.
-    enough {{ Γ ⊢ B[WkWksucc][IdNrecN] ≈ B[Id ,, succ N] : Type@i }}...
+    assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id,,succ N] : Type@i }} by mauto 4.
+    enough {{ Γ ⊢ B[WkWksucc][IdNrecN] ≈ B[Id,,succ N] : Type@i }}...
 
   - eexists...
 
@@ -124,7 +132,9 @@ Proof with mautosolve 4.
   - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Γ ⊢ B ≈ B' : Type@(max i i0) }} by mauto using lift_exp_eq_max_left.
     assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
-    enough {{ Γ ⊢ λ B' N' : Π B' C }}; mauto.
+    assert {{ Γ ⊢ Π B C ≈ Π B' C : Type@(max i i0) }} by mauto.
+    assert {{ Γ, B' ⊢ N' : C }} by mauto 4.
+    enough {{ Γ ⊢ λ B' N' : Π B' C }}...
 
   - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
@@ -139,15 +149,21 @@ Proof with mautosolve 4.
     enough {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }}...
 
   - assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
-    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
+    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
+    enough {{ Δ ⊢ Π B C : Type@(max i i0) }}...
 
-  - assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by (econstructor; mauto).
+  - assert {{ Γ ⊢s Id ≈ Id : Γ }} by mauto.
+    assert {{ Γ ⊢ B[Id] ≈ B : Type@i }} by mauto.
+    assert {{ Γ ⊢ L ≈ L' : B[Id] }} by mauto.
+    assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by mauto.
     enough {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }}...
 
-  - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto.
-    assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
-    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by (econstructor; mauto).
+  - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto 4.
+    assert {{ Δ ⊢ L : B[Id] }} by mauto 4.
+    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by mauto.
     assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto.
+    assert {{ Δ ⊢s Id ,, L : Δ, B }} by mauto.
+    assert {{ Γ ⊢s (Id ,, L)∘σ : Δ, B }} by mauto.
     assert {{ Γ ⊢ C[(Id ,, L)∘σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto.
     enough {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }}...
 
@@ -157,6 +173,8 @@ Proof with mautosolve 4.
     assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
     assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto.
     assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) ≈ σ ,, L[σ] : Δ, B }} by mauto.
+    assert {{ Γ ⊢s Id ,, L[σ] : Γ, B[σ] }} by mauto.
+    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) : Δ, B }} by mauto.
     assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
     enough {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }}...
 
@@ -170,16 +188,18 @@ Proof with mautosolve 4.
     assert {{ Γ, B ⊢ #0 : B[Wk] }} by mauto.
     assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto.
     assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id0] }} by mauto.
-    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk ∘ Id0] }} by mauto.
-    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 4.
+    assert {{ Γ, B, B[Wk] ⊢s q Wk : Γ, B }} by mauto 4.
+    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk ∘ Id0] }} by mauto 4.
+    assert {{ Γ, B ⊢ B[Wk][Id] ≈ B[Wk] : Type@i }} by mauto.
+    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 3.
     assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto.
-    assert {{ Γ, B ⊢s Wk : Γ }} by mauto.
-    assert {{ Γ, B ⊢s Wk∘Id : Γ }} by mauto.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 : Γ }} by mauto.
+    assert {{ Γ, B ⊢s Wk : Γ }} by mauto 4.
+    assert {{ Γ, B, B[Wk] ⊢s Wk∘Wk : Γ }} by mauto 4.
+    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 : Γ }} by mauto 4.
     assert {{ Γ, B, B[Wk] ⊢s Wk : Γ, B }} by mauto.
     assert {{ Γ, B ⊢s Id ≈ Wk∘Id0 : Γ, B }} by mauto.
     assert {{ Γ, B ⊢s Wk∘Id ≈ Wk∘(Wk∘Id0) : Γ }} by mauto.
-    assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘Id0 : Γ }} by mauto.
+    assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘Id0 : Γ }} by mauto 4.
     assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto 4.
     assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk∘Wk] }} by mauto 3.
     assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ (Wk∘Wk)∘Id0 ,, #0[Id0] : Γ, B }} by mauto.
@@ -201,14 +221,16 @@ Proof with mautosolve 4.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
     assert {{ ⊢ Δ, B }} by mauto.
     assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
-    assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto 4.
+    assert {{ Γ ⊢s σ ,, N' : Δ, B }} by mauto.
+    assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto 3.
     enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
 
-  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto 4.
+  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto 3.
     assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto.
     assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
-    assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto 4.
+    assert {{ Γ ⊢s σ ,, N : Δ, B }} by mauto.
+    assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto 3.
     assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto 4.
     enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
 
@@ -233,11 +255,10 @@ Proof with mautosolve 4.
 Qed.
 
 #[export]
-  Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
-
+Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 
 #[local]
-  Ltac invert_wf_ctx1 H :=
+Ltac invert_wf_ctx1 H :=
   match type of H with
   | {{ ⊢ ~_ , ~_ }} =>
       let H' := fresh "H" in
@@ -253,7 +274,6 @@ Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq H.
 
 Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx;  clear_dups.
 
-
 Lemma wf_ctx_eq_extend' : forall (Γ Δ : ctx) (A : typ) (i : nat) (A' : typ),
     {{ ⊢ Γ ≈ Δ }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
@@ -264,6 +284,6 @@ Proof.
 Qed.
 
 #[export]
-  Hint Resolve wf_ctx_eq_extend' : mcltt.
+Hint Resolve wf_ctx_eq_extend' : mcltt.
 #[export]
-  Remove Hints wf_ctx_eq_extend : mcltt.
+Remove Hints wf_ctx_eq_extend : mcltt.