diff --git a/ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html b/ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html index e71232b..b82eb8d 100644 --- a/ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html +++ b/ext/prop-eq/Mcltt.Core.Syntactic.System.Lemmas.html @@ -45,7 +45,17 @@

Mcltt.Core.Syntactic.System.Lemmas

-Lemma ctx_decomp : forall {Γ A}, {{ Γ , A }} -> {{ Γ }} /\ exists i, {{ Γ A : Type@i }}.
+Lemma ctx_lookup_lt : forall {Γ A x},
+    {{ #x : A Γ }} ->
+    x < length Γ.
+Proof.
+  induction 1; simpl; lia.
+Qed.
+#[export]
+Hint Resolve ctx_lookup_lt : mcltt.
+ +
+Lemma ctx_decomp : forall {Γ A}, {{ Γ , A }} -> {{ Γ }} /\ exists i, {{ Γ A : Type@i }}.
Proof with now eauto.
  inversion 1...
Qed.
@@ -55,13 +65,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve ctx_decomp : mcltt.

-Corollary ctx_decomp_left : forall {Γ A}, {{ Γ , A }} -> {{ Γ }}.
+Corollary ctx_decomp_left : forall {Γ A}, {{ Γ , A }} -> {{ Γ }}.
Proof with easy.
  intros * ?%ctx_decomp...
Qed.

-Corollary ctx_decomp_right : forall {Γ A}, {{ Γ , A }} -> exists i, {{ Γ A : Type@i }}.
+Corollary ctx_decomp_right : forall {Γ A}, {{ Γ , A }} -> exists i, {{ Γ A : Type@i }}.
Proof with easy.
  intros * ?%ctx_decomp...
Qed.
@@ -80,19 +90,19 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma presup_ctx_eq : forall {Γ Δ}, {{ Γ Δ }} -> {{ Γ }} /\ {{ Δ }}.
+Lemma presup_ctx_eq : forall {Γ Δ}, {{ Γ Δ }} -> {{ Γ }} /\ {{ Δ }}.
Proof with mautosolve.
  induction 1; destruct_pairs...
Qed.

-Corollary presup_ctx_eq_left : forall {Γ Δ}, {{ Γ Δ }} -> {{ Γ }}.
+Corollary presup_ctx_eq_left : forall {Γ Δ}, {{ Γ Δ }} -> {{ Γ }}.
Proof with easy.
  intros * ?%presup_ctx_eq...
Qed.

-Corollary presup_ctx_eq_right : forall {Γ Δ}, {{ Γ Δ }} -> {{ Δ }}.
+Corollary presup_ctx_eq_right : forall {Γ Δ}, {{ Γ Δ }} -> {{ Δ }}.
Proof with easy.
  intros * ?%presup_ctx_eq...
Qed.
@@ -102,19 +112,19 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.

-Lemma presup_sub : forall {Γ Δ σ}, {{ Γ s σ : Δ }} -> {{ Γ }} /\ {{ Δ }}.
+Lemma presup_sub : forall {Γ Δ σ}, {{ Γ s σ : Δ }} -> {{ Γ }} /\ {{ Δ }}.
Proof with mautosolve.
  induction 1; destruct_pairs...
Qed.

-Corollary presup_sub_left : forall {Γ Δ σ}, {{ Γ s σ : Δ }} -> {{ Γ }}.
+Corollary presup_sub_left : forall {Γ Δ σ}, {{ Γ s σ : Δ }} -> {{ Γ }}.
Proof with easy.
  intros * ?%presup_sub...
Qed.

-Corollary presup_sub_right : forall {Γ Δ σ}, {{ Γ s σ : Δ }} -> {{ Δ }}.
+Corollary presup_sub_right : forall {Γ Δ σ}, {{ Γ s σ : Δ }} -> {{ Δ }}.
Proof with easy.
  intros * ?%presup_sub...
Qed.
@@ -132,7 +142,7 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma presup_exp_ctx : forall {Γ M A}, {{ Γ M : A }} -> {{ Γ }}.
+Lemma presup_exp_ctx : forall {Γ M A}, {{ Γ M : A }} -> {{ Γ }}.
Proof with mautosolve.
  induction 1...
Qed.
@@ -150,19 +160,19 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ s σ σ' : Δ }} -> {{ Γ }} /\ {{ Δ }}.
+Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ s σ σ' : Δ }} -> {{ Γ }} /\ {{ Δ }}.
Proof with mautosolve.
  induction 1; destruct_pairs...
Qed.

-Corollary presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ s σ σ' : Δ }} -> {{ Γ }}.
+Corollary presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ s σ σ' : Δ }} -> {{ Γ }}.
Proof with easy.
  intros * ?%presup_sub_eq_ctx...
Qed.

-Corollary presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ s σ σ' : Δ }} -> {{ Δ }}.
+Corollary presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ s σ σ' : Δ }} -> {{ Δ }}.
Proof with easy.
  intros * ?%presup_sub_eq_ctx...
Qed.
@@ -172,7 +182,7 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve presup_sub_eq_ctx presup_sub_eq_ctx_left presup_sub_eq_ctx_right : mcltt.

-Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ M M' : A }} -> {{ Γ }}.
+Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ M M' : A }} -> {{ Γ }}.
Proof with mautosolve 2.
  induction 1...
Qed.
@@ -195,21 +205,21 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma wf_cumu : forall Γ A i,
-    {{ Γ A : Type@i }} ->
-    {{ Γ A : Type@(S i) }}.
+Lemma wf_cumu : forall Γ A i,
+    {{ Γ A : Type@i }} ->
+    {{ Γ A : Type@(S i) }}.
Proof with mautosolve.
  intros.
-  enough {{ Γ }}...
+  enough {{ Γ }}...
Qed.

-Lemma wf_exp_eq_cumu : forall Γ A A' i,
-    {{ Γ A A' : Type@i }} ->
-    {{ Γ A A' : Type@(S i) }}.
+Lemma wf_exp_eq_cumu : forall Γ A A' i,
+    {{ Γ A A' : Type@i }} ->
+    {{ Γ A A' : Type@(S i) }}.
Proof with mautosolve.
  intros.
-  enough {{ Γ }}...
+  enough {{ Γ }}...
Qed.

@@ -217,9 +227,9 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_cumu wf_exp_eq_cumu : mcltt.

-Lemma wf_ctx_sub_refl : forall Γ Δ,
-    {{ Γ Δ }} ->
-    {{ Γ Δ }}.
+Lemma wf_ctx_sub_refl : forall Γ Δ,
+    {{ Γ Δ }} ->
+    {{ Γ Δ }}.
Proof. induction 1; mauto. Qed.

@@ -227,17 +237,17 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_ctx_sub_refl : mcltt.

-Lemma wf_conv : forall Γ M A i A',
-    {{ Γ M : A }} ->
+Lemma wf_conv : forall Γ M A i A',
+    {{ Γ M : A }} ->
    
The next argument will be removed in SystemOpt
-    {{ Γ A' : Type@i }} ->
-    {{ Γ A A' : Type@i }} ->
-    {{ Γ M : A' }}.
+    {{ Γ A' : Type@i }} ->
+    {{ Γ A A' : Type@i }} ->
+    {{ Γ M : A' }}.
Proof. mauto. Qed.

@@ -245,10 +255,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_conv : mcltt.

-Lemma wf_sub_conv : forall Γ σ Δ Δ',
-  {{ Γ s σ : Δ }} ->
-  {{ Δ Δ' }} ->
-  {{ Γ s σ : Δ' }}.
+Lemma wf_sub_conv : forall Γ σ Δ Δ',
+  {{ Γ s σ : Δ }} ->
+  {{ Δ Δ' }} ->
+  {{ Γ s σ : Δ' }}.
Proof. mauto. Qed.

@@ -256,17 +266,17 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_sub_conv : mcltt.

-Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
-   {{ Γ M M' : A }} ->
+Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
+   {{ Γ M M' : A }} ->
   
The next argument will be removed in SystemOpt
-   {{ Γ A' : Type@i }} ->
-   {{ Γ A A' : Type@i }} ->
-   {{ Γ M M' : A' }}.
+   {{ Γ A' : Type@i }} ->
+   {{ Γ A A' : Type@i }} ->
+   {{ Γ M M' : A' }}.
Proof. mauto. Qed.

@@ -274,10 +284,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_exp_eq_conv : mcltt.

-Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ',
-    {{ Γ s σ σ' : Δ }} ->
-    {{ Δ Δ' }} ->
-    {{ Γ s σ σ' : Δ' }}.
+Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ',
+    {{ Γ s σ σ' : Δ }} ->
+    {{ Δ Δ' }} ->
+    {{ Γ s σ σ' : Δ' }}.
Proof. mauto. Qed.

@@ -285,7 +295,7 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_sub_eq_conv : mcltt.

-Add Parametric Morphism Γ : (wf_sub_eq Γ)
+Add Parametric Morphism Γ : (wf_sub_eq Γ)
    with signature wf_ctx_eq ==> eq ==> eq ==> iff as wf_sub_eq_morphism_iff3.
Proof.
  intros Δ Δ' H **; split; [| symmetry in H]; mauto.
@@ -300,10 +310,10 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma lift_exp_ge : forall {Γ A n m},
-    n <= m ->
-    {{ Γ A : Type@n }} ->
-    {{ Γ A : Type@m }}.
+Lemma lift_exp_ge : forall {Γ A n m},
+    n <= m ->
+    {{ Γ A : Type@n }} ->
+    {{ Γ A : Type@m }}.
Proof with mautosolve.
  induction 1...
Qed.
@@ -313,28 +323,28 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve lift_exp_ge : mcltt.

-Corollary lift_exp_max_left : forall {Γ A n} m,
-    {{ Γ A : Type@n }} ->
-    {{ Γ A : Type@(max n m) }}.
+Corollary lift_exp_max_left : forall {Γ A n} m,
+    {{ Γ A : Type@n }} ->
+    {{ Γ A : Type@(max n m) }}.
Proof with mautosolve.
  intros.
  assert (n <= max n m) by lia...
Qed.

-Corollary lift_exp_max_right : forall {Γ A} n {m},
-    {{ Γ A : Type@m }} ->
-    {{ Γ A : Type@(max n m) }}.
+Corollary lift_exp_max_right : forall {Γ A} n {m},
+    {{ Γ A : Type@m }} ->
+    {{ Γ A : Type@(max n m) }}.
Proof with mautosolve.
  intros.
  assert (m <= max n m) by lia...
Qed.

-Lemma lift_exp_eq_ge : forall {Γ A A' n m},
-    n <= m ->
-    {{ Γ A A': Type@n }} ->
-    {{ Γ A A' : Type@m }}.
+Lemma lift_exp_eq_ge : forall {Γ A A' n m},
+    n <= m ->
+    {{ Γ A A': Type@n }} ->
+    {{ Γ A A' : Type@m }}.
Proof with mautosolve.
  induction 1; subst...
Qed.
@@ -344,18 +354,18 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve lift_exp_eq_ge : mcltt.

-Corollary lift_exp_eq_max_left : forall {Γ A A' n} m,
-    {{ Γ A A' : Type@n }} ->
-    {{ Γ A A' : Type@(max n m) }}.
+Corollary lift_exp_eq_max_left : forall {Γ A A' n} m,
+    {{ Γ A A' : Type@n }} ->
+    {{ Γ A A' : Type@(max n m) }}.
Proof with mautosolve.
  intros.
  assert (n <= max n m) by lia...
Qed.

-Corollary lift_exp_eq_max_right : forall {Γ A A'} n {m},
-    {{ Γ A A' : Type@m }} ->
-    {{ Γ A A' : Type@(max n m) }}.
+Corollary lift_exp_eq_max_right : forall {Γ A A'} n {m},
+    {{ Γ A A' : Type@m }} ->
+    {{ Γ A A' : Type@(max n m) }}.
Proof with mautosolve.
  intros.
  assert (m <= max n m) by lia...
@@ -371,9 +381,9 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma exp_eq_refl : forall {Γ M A},
-    {{ Γ M : A }} ->
-    {{ Γ M M : A }}.
+Lemma exp_eq_refl : forall {Γ M A},
+    {{ Γ M : A }} ->
+    {{ Γ M M : A }}.
Proof. mauto. Qed.

@@ -381,14 +391,14 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_refl : mcltt.

-Lemma exp_eq_trans_typ_max : forall {Γ i i' A A' A''},
-    {{ Γ A A' : Type@i }} ->
-    {{ Γ A' A'' : Type@i' }} ->
-    {{ Γ A A'' : Type@(max i i') }}.
+Lemma exp_eq_trans_typ_max : forall {Γ i i' A A' A''},
+    {{ Γ A A' : Type@i }} ->
+    {{ Γ A' A'' : Type@i' }} ->
+    {{ Γ A A'' : Type@(max i i') }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ A A' : Type@(max i i') }} by eauto using lift_exp_eq_max_left.
-  assert {{ Γ A' A'' : Type@(max i i') }} by eauto using lift_exp_eq_max_right...
+  assert {{ Γ A A' : Type@(max i i') }} by eauto using lift_exp_eq_max_left.
+  assert {{ Γ A' A'' : Type@(max i i') }} by eauto using lift_exp_eq_max_right...
Qed.

@@ -396,9 +406,9 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_trans_typ_max : mcltt.

-Lemma sub_eq_refl : forall {Γ σ Δ},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ s σ σ : Δ }}.
+Lemma sub_eq_refl : forall {Γ σ Δ},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ s σ σ : Δ }}.
Proof. mauto. Qed.

@@ -415,10 +425,10 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma exp_sub_typ : forall {Δ Γ A σ i},
-    {{ Δ A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ A[σ] : Type@i }}.
+Lemma exp_sub_typ : forall {Δ Γ A σ i},
+    {{ Δ A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ A[σ] : Type@i }}.
Proof with mautosolve 3.
  intros.
  econstructor; mauto 3.
@@ -430,15 +440,15 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_sub_typ : mcltt.

-Lemma presup_ctx_lookup_typ : forall {Γ A x},
-    {{ Γ }} ->
-    {{ #x : A Γ }} ->
-    exists i, {{ Γ A : Type@i }}.
+Lemma presup_ctx_lookup_typ : forall {Γ A x},
+    {{ Γ }} ->
+    {{ #x : A Γ }} ->
+    exists i, {{ Γ A : Type@i }}.
Proof with mautosolve 4.
  intros * .
  induction 1; inversion_clear ;
-    [assert {{ Γ, A Type@i[Wk] Type@i : Type@(S i) }} by mauto 4
-    | assert (exists i, {{ Γ A : Type@i }}) as [] by eauto]; econstructor...
+    [assert {{ Γ, A Type@i[Wk] Type@i : Type@(S i) }} by mauto 4
+    | assert (exists i, {{ Γ A : Type@i }}) as [] by eauto]; econstructor...
Qed.

@@ -446,32 +456,32 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve presup_ctx_lookup_typ : mcltt.

-Lemma exp_eq_sub_cong_typ1 : forall {Δ Γ A A' σ i},
-    {{ Δ A A' : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ A[σ] A'[σ] : Type@i }}.
+Lemma exp_eq_sub_cong_typ1 : forall {Δ Γ A A' σ i},
+    {{ Δ A A' : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ A[σ] A'[σ] : Type@i }}.
Proof with mautosolve 3.
  intros.
  eapply wf_exp_eq_conv...
Qed.

-Lemma exp_eq_sub_cong_typ2' : forall {Δ Γ A σ τ i},
-    {{ Δ A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ s σ τ : Δ }} ->
-    {{ Γ A[σ] A[τ] : Type@i }}.
+Lemma exp_eq_sub_cong_typ2' : forall {Δ Γ A σ τ i},
+    {{ Δ A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ s σ τ : Δ }} ->
+    {{ Γ A[σ] A[τ] : Type@i }}.
Proof with mautosolve 3.
  intros.
  eapply wf_exp_eq_conv...
Qed.

-Lemma exp_eq_sub_compose_typ : forall {Ψ Δ Γ A σ τ i},
-    {{ Ψ A : Type@i }} ->
-    {{ Δ s σ : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ A[σ][τ] A[στ] : Type@i }}.
+Lemma exp_eq_sub_compose_typ : forall {Ψ Δ Γ A σ τ i},
+    {{ Ψ A : Type@i }} ->
+    {{ Δ s σ : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ A[σ][τ] A[στ] : Type@i }}.
Proof with mautosolve 3.
  intros.
  eapply wf_exp_eq_conv...
@@ -482,10 +492,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mcltt.

-Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i},
-    {{ Δ s σ : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ Type@i[σ][τ] Type@i : Type@(S i) }}.
+Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i},
+    {{ Δ s σ : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ Type@i[σ][τ] Type@i : Type@(S i) }}.
Proof. mauto. Qed.

@@ -495,10 +505,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Rewrite -> @exp_eq_sub_compose_typ @exp_eq_typ_sub_sub using mauto 4 : mcltt.

-Lemma functional_ctx_lookup : forall {Γ A A' x},
-    {{ #x : A Γ }} ->
-    {{ #x : A' Γ }} ->
-    A = A'.
+Lemma functional_ctx_lookup : forall {Γ A A' x},
+    {{ #x : A Γ }} ->
+    {{ #x : A' Γ }} ->
+    A = A'.
Proof with mautosolve.
  intros * Hx Hx'; gen A'.
  induction Hx as [|* ? IHHx]; intros; inversion_clear Hx';
@@ -507,9 +517,9 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma vlookup_0_typ : forall {Γ i},
-    {{ Γ }} ->
-    {{ Γ, Type@i # 0 : Type@i }}.
+Lemma vlookup_0_typ : forall {Γ i},
+    {{ Γ }} ->
+    {{ Γ, Type@i # 0 : Type@i }}.
Proof with mautosolve 4.
  intros.
  eapply wf_conv; mauto 4.
@@ -517,13 +527,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma vlookup_1_typ : forall {Γ i A j},
-    {{ Γ, Type@i A : Type@j }} ->
-    {{ Γ, Type@i, A # 1 : Type@i }}.
+Lemma vlookup_1_typ : forall {Γ i A j},
+    {{ Γ, Type@i A : Type@j }} ->
+    {{ Γ, Type@i, A # 1 : Type@i }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ, Type@i s Wk : Γ }} by mauto 4.
-  assert {{ Γ, Type@i, A s Wk : Γ, Type@i }} by mauto 4.
+  assert {{ Γ, Type@i s Wk : Γ }} by mauto 4.
+  assert {{ Γ, Type@i, A s Wk : Γ, Type@i }} by mauto 4.
  eapply wf_conv...
Qed.
@@ -532,10 +542,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve vlookup_0_typ vlookup_1_typ : mcltt.

-Lemma exp_sub_typ_helper : forall {Γ σ Δ M i},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : Type@i }} ->
-    {{ Γ M : Type@i[σ] }}.
+Lemma exp_sub_typ_helper : forall {Γ σ Δ M i},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : Type@i }} ->
+    {{ Γ M : Type@i[σ] }}.
Proof.
  intros.
  do 2 (econstructor; mauto 4).
@@ -546,10 +556,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_sub_typ_helper : mcltt.

-Lemma exp_eq_var_0_sub_typ : forall {Γ σ Δ M i},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : Type@i }} ->
-    {{ Γ #0[σ,,M] M : Type@i }}.
+Lemma exp_eq_var_0_sub_typ : forall {Γ σ Δ M i},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : Type@i }} ->
+    {{ Γ #0[σ,,M] M : Type@i }}.
Proof with mautosolve 4.
  intros.
  eapply wf_exp_eq_conv; mauto 3.
@@ -557,16 +567,16 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma exp_eq_var_1_sub_typ : forall {Γ σ Δ A i M j},
-    {{ Γ s σ : Δ }} ->
-    {{ Δ A : Type@i }} ->
-    {{ Γ M : A[σ] }} ->
-    {{ #0 : Type@j[Wk] Δ }} ->
-    {{ Γ #1[σ,,M] #0[σ] : Type@j }}.
+Lemma exp_eq_var_1_sub_typ : forall {Γ σ Δ A i M j},
+    {{ Γ s σ : Δ }} ->
+    {{ Δ A : Type@i }} ->
+    {{ Γ M : A[σ] }} ->
+    {{ #0 : Type@j[Wk] Δ }} ->
+    {{ Γ #1[σ,,M] #0[σ] : Type@j }}.
Proof with mautosolve 4.
  inversion 4 as [? Δ'|]; subst.
-  assert {{ Δ' }} by mauto 4.
-  assert {{ Δ', Type@j s Wk : Δ' }} by mauto 4.
+  assert {{ Δ' }} by mauto 4.
+  assert {{ Δ', Type@j s Wk : Δ' }} by mauto 4.
  eapply wf_exp_eq_conv...
Qed.
@@ -577,16 +587,16 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Rewrite -> @exp_eq_var_0_sub_typ @exp_eq_var_1_sub_typ : mcltt.

-Lemma exp_eq_var_0_weaken_typ : forall {Γ A i},
-    {{ Γ, A }} ->
-    {{ #0 : Type@i[Wk] Γ }} ->
-    {{ Γ, A #0[Wk] #1 : Type@i }}.
+Lemma exp_eq_var_0_weaken_typ : forall {Γ A i},
+    {{ Γ, A }} ->
+    {{ #0 : Type@i[Wk] Γ }} ->
+    {{ Γ, A #0[Wk] #1 : Type@i }}.
Proof with mautosolve 3.
  inversion_clear 1.
  inversion 1 as [? Γ'|]; subst.
-  assert {{ Γ' }} by mauto.
-  assert {{ Γ', Type@i s Wk : Γ' }} by mauto 4.
-  assert {{ Γ', Type@i, A s Wk : Γ', Type@i }} by mauto 4.
+  assert {{ Γ' }} by mauto.
+  assert {{ Γ', Type@i s Wk : Γ' }} by mauto 4.
+  assert {{ Γ', Type@i, A s Wk : Γ', Type@i }} by mauto 4.
  eapply wf_exp_eq_conv...
Qed.
@@ -595,10 +605,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_var_0_weaken_typ : mcltt.

-Lemma sub_extend_typ : forall {Γ σ Δ M i},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : Type@i }} ->
-    {{ Γ s σ,,M : Δ, Type@i }}.
+Lemma sub_extend_typ : forall {Γ σ Δ M i},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : Type@i }} ->
+    {{ Γ s σ,,M : Δ, Type@i }}.
Proof with mautosolve 4.
  intros.
  econstructor...
@@ -609,11 +619,11 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_extend_typ : mcltt.

-Lemma sub_eq_extend_cong_typ : forall {Γ σ σ' Δ M M' i},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ s σ σ' : Δ }} ->
-    {{ Γ M M' : Type@i }} ->
-    {{ Γ s σ,,M σ',,M' : Δ, Type@i }}.
+Lemma sub_eq_extend_cong_typ : forall {Γ σ σ' Δ M M' i},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ s σ σ' : Δ }} ->
+    {{ Γ M M' : Type@i }} ->
+    {{ Γ s σ,,M σ',,M' : Δ, Type@i }}.
Proof with mautosolve 4.
  intros.
  econstructor; mauto 3.
@@ -621,25 +631,25 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma sub_eq_extend_compose_typ : forall {Γ τ Γ' σ Γ'' A i M j},
-    {{ Γ' s σ : Γ'' }} ->
-    {{ Γ'' A : Type@i }} ->
-    {{ Γ' M : Type@j }} ->
-    {{ Γ s τ : Γ' }} ->
-    {{ Γ s (σ,,M) τ (σ τ),,M[τ] : Γ'', Type@j }}.
+Lemma sub_eq_extend_compose_typ : forall {Γ τ Γ' σ Γ'' A i M j},
+    {{ Γ' s σ : Γ'' }} ->
+    {{ Γ'' A : Type@i }} ->
+    {{ Γ' M : Type@j }} ->
+    {{ Γ s τ : Γ' }} ->
+    {{ Γ s (σ,,M) τ (σ τ),,M[τ] : Γ'', Type@j }}.
Proof with mautosolve 4.
  intros.
  econstructor...
Qed.

-Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i},
-    {{ Γ' s σ : Γ }} ->
-    {{ Γ' M : Type@i }} ->
-    {{ Γ' s Wk (σ,,M) σ : Γ }}.
+Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i},
+    {{ Γ' s σ : Γ }} ->
+    {{ Γ' M : Type@i }} ->
+    {{ Γ' s Wk (σ,,M) σ : Γ }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ Type@i : Type@(S i) }} by mauto.
+  assert {{ Γ Type@i : Type@(S i) }} by mauto.
  econstructor; mauto 3.
Qed.
@@ -648,15 +658,15 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_extend_cong_typ sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt.

-Lemma sub_eq_wk_var0_id : forall {Γ A i},
-    {{ Γ A : Type@i }} ->
-    {{ Γ, A s Wk,,#0 Id : Γ, A }}.
+Lemma sub_eq_wk_var0_id : forall {Γ A i},
+    {{ Γ A : Type@i }} ->
+    {{ Γ, A s Wk,,#0 Id : Γ, A }}.
Proof with mautosolve 4.
  intros * ?.
-  assert {{ Γ, A }} by mauto 3.
-  assert {{ Γ, A s (WkId),,#0[Id] Id : Γ, A }} by mauto.
-  assert {{ Γ, A s Wk WkId : Γ }} by mauto.
-  enough {{ Γ, A #0 #0[Id] : A[Wk] }}...
+  assert {{ Γ, A }} by mauto 3.
+  assert {{ Γ, A s (WkId),,#0[Id] Id : Γ, A }} by mauto.
+  assert {{ Γ, A s Wk WkId : Γ }} by mauto.
+  enough {{ Γ, A #0 #0[Id] : A[Wk] }}...
Qed.

@@ -666,19 +676,19 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Rewrite -> @sub_eq_wk_var0_id using mauto 4 : mcltt.

-Lemma exp_eq_sub_sub_compose_cong_typ : forall {Γ Δ Δ' Ψ σ τ σ' τ' A i},
-    {{ Ψ A : Type@i }} ->
-    {{ Δ s σ : Ψ }} ->
-    {{ Δ' s σ' : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ s τ' : Δ' }} ->
-    {{ Γ s στ σ'τ' : Ψ }} ->
-    {{ Γ A[σ][τ] A[σ'][τ'] : Type@i }}.
+Lemma exp_eq_sub_sub_compose_cong_typ : forall {Γ Δ Δ' Ψ σ τ σ' τ' A i},
+    {{ Ψ A : Type@i }} ->
+    {{ Δ s σ : Ψ }} ->
+    {{ Δ' s σ' : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ s τ' : Δ' }} ->
+    {{ Γ s στ σ'τ' : Ψ }} ->
+    {{ Γ A[σ][τ] A[σ'][τ'] : Type@i }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ A[σ][τ] A[στ] : Type@i }} by mauto.
-  assert {{ Γ A[στ] A[σ'τ'] : Type@i }} by mauto.
-  enough {{ Γ A[σ'τ'] A[σ'][τ'] : Type@i }}...
+  assert {{ Γ A[σ][τ] A[στ] : Type@i }} by mauto.
+  assert {{ Γ A[στ] A[σ'τ'] : Type@i }} by mauto.
+  enough {{ Γ A[σ'τ'] A[σ'][τ'] : Type@i }}...
Qed.

@@ -695,10 +705,10 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma exp_sub_nat : forall {Δ Γ M σ},
-    {{ Δ M : }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M[σ] : }}.
+Lemma exp_sub_nat : forall {Δ Γ M σ},
+    {{ Δ M : }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M[σ] : }}.
Proof with mautosolve 3.
  intros.
  econstructor; mauto 3.
@@ -710,32 +720,32 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_sub_nat : mcltt.

-Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ},
-    {{ Δ M M' : }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M[σ] M'[σ] : }}.
+Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ},
+    {{ Δ M M' : }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M[σ] M'[σ] : }}.
Proof with mautosolve 3.
  intros.
  eapply wf_exp_eq_conv...
Qed.

-Lemma exp_eq_sub_cong_nat2 : forall {Δ Γ M σ τ},
-    {{ Δ M : }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ s σ τ : Δ }} ->
-    {{ Γ M[σ] M[τ] : }}.
+Lemma exp_eq_sub_cong_nat2 : forall {Δ Γ M σ τ},
+    {{ Δ M : }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ s σ τ : Δ }} ->
+    {{ Γ M[σ] M[τ] : }}.
Proof with mautosolve.
  intros.
  eapply wf_exp_eq_conv...
Qed.

-Lemma exp_eq_sub_compose_nat : forall {Ψ Δ Γ M σ τ},
-    {{ Ψ M : }} ->
-    {{ Δ s σ : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ M[σ][τ] M[στ] : }}.
+Lemma exp_eq_sub_compose_nat : forall {Ψ Δ Γ M σ τ},
+    {{ Ψ M : }} ->
+    {{ Δ s σ : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ M[σ][τ] M[στ] : }}.
Proof with mautosolve 4.
  intros.
  eapply wf_exp_eq_conv...
@@ -746,10 +756,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_sub_nat exp_eq_sub_cong_nat1 exp_eq_sub_cong_nat2 exp_eq_sub_compose_nat : mcltt.

-Lemma exp_eq_nat_sub_sub : forall {Γ Δ Ψ σ τ},
-    {{ Δ s σ : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ [σ][τ] : Type@0 }}.
+Lemma exp_eq_nat_sub_sub : forall {Γ Δ Ψ σ τ},
+    {{ Δ s σ : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ [σ][τ] : Type@0 }}.
Proof. mauto. Qed.

@@ -757,11 +767,11 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_nat_sub_sub : mcltt.

-Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ'},
-    {{ Δ s σ : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ s σ' : Ψ' }} ->
-    {{ Γ [σ][τ] [σ'] : Type@0 }}.
+Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ'},
+    {{ Δ s σ : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ s σ' : Ψ' }} ->
+    {{ Γ [σ][τ] [σ'] : Type@0 }}.
Proof. mauto. Qed.

@@ -769,9 +779,9 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt.

-Lemma vlookup_0_nat : forall {Γ},
-    {{ Γ }} ->
-    {{ Γ, # 0 : }}.
+Lemma vlookup_0_nat : forall {Γ},
+    {{ Γ }} ->
+    {{ Γ, # 0 : }}.
Proof with mautosolve 4.
  intros.
  eapply wf_conv; mauto 4.
@@ -779,13 +789,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma vlookup_1_nat : forall {Γ A i},
-    {{ Γ, A : Type@i }} ->
-    {{ Γ, , A # 1 : }}.
+Lemma vlookup_1_nat : forall {Γ A i},
+    {{ Γ, A : Type@i }} ->
+    {{ Γ, , A # 1 : }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ, s Wk : Γ }} by mauto 4.
-  assert {{ Γ, , A s Wk : Γ, }} by mauto 4.
+  assert {{ Γ, s Wk : Γ }} by mauto 4.
+  assert {{ Γ, , A s Wk : Γ, }} by mauto 4.
  eapply wf_conv...
Qed.
@@ -794,10 +804,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve vlookup_0_nat vlookup_1_nat : mcltt.

-Lemma exp_sub_nat_helper : forall {Γ σ Δ M},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : }} ->
-    {{ Γ M : [σ] }}.
+Lemma exp_sub_nat_helper : forall {Γ σ Δ M},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : }} ->
+    {{ Γ M : [σ] }}.
Proof.
  intros.
  do 2 (econstructor; mauto 4).
@@ -808,10 +818,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_sub_nat_helper : mcltt.

-Lemma exp_eq_var_0_sub_nat : forall {Γ σ Δ M},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : }} ->
-    {{ Γ #0[σ,,M] M : }}.
+Lemma exp_eq_var_0_sub_nat : forall {Γ σ Δ M},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : }} ->
+    {{ Γ #0[σ,,M] M : }}.
Proof with mautosolve 3.
  intros.
  eapply wf_exp_eq_conv; mauto 3.
@@ -819,16 +829,16 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma exp_eq_var_1_sub_nat : forall {Γ σ Δ A i M},
-    {{ Γ s σ : Δ }} ->
-    {{ Δ A : Type@i }} ->
-    {{ Γ M : A[σ] }} ->
-    {{ #0 : [Wk] Δ }} ->
-    {{ Γ #1[σ,,M] #0[σ] : }}.
+Lemma exp_eq_var_1_sub_nat : forall {Γ σ Δ A i M},
+    {{ Γ s σ : Δ }} ->
+    {{ Δ A : Type@i }} ->
+    {{ Γ M : A[σ] }} ->
+    {{ #0 : [Wk] Δ }} ->
+    {{ Γ #1[σ,,M] #0[σ] : }}.
Proof with mautosolve 4.
  inversion 4 as [? Δ'|]; subst.
-  assert {{ Γ #1[σ,, M] #0[σ] : [Wk][σ] }} by mauto 4.
-  assert {{ Γ [Wk][σ] : Type@0 }}...
+  assert {{ Γ #1[σ,, M] #0[σ] : [Wk][σ] }} by mauto 4.
+  assert {{ Γ [Wk][σ] : Type@0 }}...
Qed.

@@ -836,15 +846,15 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_var_0_sub_nat exp_eq_var_1_sub_nat : mcltt.

-Lemma exp_eq_var_0_weaken_nat : forall {Γ A},
-    {{ Γ, A }} ->
-    {{ #0 : [Wk] Γ }} ->
-    {{ Γ, A #0[Wk] #1 : }}.
+Lemma exp_eq_var_0_weaken_nat : forall {Γ A},
+    {{ Γ, A }} ->
+    {{ #0 : [Wk] Γ }} ->
+    {{ Γ, A #0[Wk] #1 : }}.
Proof with mautosolve 4.
  inversion 1; subst.
  inversion 1 as [? Γ'|]; subst.
-  assert {{ Γ', , A #0[Wk] # 1 : [Wk][Wk] }} by mauto 4.
-  assert {{ Γ', , A [Wk][Wk] : Type@0 }}...
+  assert {{ Γ', , A #0[Wk] # 1 : [Wk][Wk] }} by mauto 4.
+  assert {{ Γ', , A [Wk][Wk] : Type@0 }}...
Qed.

@@ -852,10 +862,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_var_0_weaken_nat : mcltt.

-Lemma sub_extend_nat : forall {Γ σ Δ M},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : }} ->
-    {{ Γ s σ,,M : Δ , }}.
+Lemma sub_extend_nat : forall {Γ σ Δ M},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : }} ->
+    {{ Γ s σ,,M : Δ , }}.
Proof with mautosolve 3.
  intros.
  econstructor...
@@ -866,11 +876,11 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_extend_nat : mcltt.

-Lemma sub_eq_extend_cong_nat : forall {Γ σ σ' Δ M M'},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ s σ σ' : Δ }} ->
-    {{ Γ M M' : }} ->
-    {{ Γ s σ,,M σ',,M' : Δ , }}.
+Lemma sub_eq_extend_cong_nat : forall {Γ σ σ' Δ M M'},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ s σ σ' : Δ }} ->
+    {{ Γ M M' : }} ->
+    {{ Γ s σ,,M σ',,M' : Δ , }}.
Proof with mautosolve 4.
  intros.
  econstructor; mauto 3.
@@ -878,24 +888,24 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma sub_eq_extend_compose_nat : forall {Γ τ Γ' σ Γ'' M},
-    {{ Γ' s σ : Γ'' }} ->
-    {{ Γ' M : }} ->
-    {{ Γ s τ : Γ' }} ->
-    {{ Γ s (σ,,M) τ (σ τ),,M[τ] : Γ'' , }}.
+Lemma sub_eq_extend_compose_nat : forall {Γ τ Γ' σ Γ'' M},
+    {{ Γ' s σ : Γ'' }} ->
+    {{ Γ' M : }} ->
+    {{ Γ s τ : Γ' }} ->
+    {{ Γ s (σ,,M) τ (σ τ),,M[τ] : Γ'' , }}.
Proof with mautosolve 3.
  intros.
  econstructor...
Qed.

-Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M},
-    {{ Γ' s σ : Γ }} ->
-    {{ Γ' M : }} ->
-    {{ Γ' s Wk (σ,,M) σ : Γ }}.
+Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M},
+    {{ Γ' s σ : Γ }} ->
+    {{ Γ' M : }} ->
+    {{ Γ' s Wk (σ,,M) σ : Γ }}.
Proof with mautosolve 3.
  intros.
-  assert {{ Γ : Type@0 }} by mauto.
+  assert {{ Γ : Type@0 }} by mauto.
  econstructor...
Qed.
@@ -904,19 +914,19 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_extend_cong_nat sub_eq_extend_compose_nat sub_eq_p_extend_nat : mcltt.

-Lemma exp_eq_sub_sub_compose_cong_nat : forall {Γ Δ Δ' Ψ σ τ σ' τ' M},
-    {{ Ψ M : }} ->
-    {{ Δ s σ : Ψ }} ->
-    {{ Δ' s σ' : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ s τ' : Δ' }} ->
-    {{ Γ s στ σ'τ' : Ψ }} ->
-    {{ Γ M[σ][τ] M[σ'][τ'] : }}.
+Lemma exp_eq_sub_sub_compose_cong_nat : forall {Γ Δ Δ' Ψ σ τ σ' τ' M},
+    {{ Ψ M : }} ->
+    {{ Δ s σ : Ψ }} ->
+    {{ Δ' s σ' : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ s τ' : Δ' }} ->
+    {{ Γ s στ σ'τ' : Ψ }} ->
+    {{ Γ M[σ][τ] M[σ'][τ'] : }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ M[σ][τ] M[στ] : }} by mauto.
-  assert {{ Γ M[στ] M[σ'τ'] : }} by mauto.
-  enough {{ Γ M[σ'τ'] M[σ'][τ'] : }}...
+  assert {{ Γ M[σ][τ] M[στ] : }} by mauto.
+  assert {{ Γ M[στ] M[σ'τ'] : }} by mauto.
+  enough {{ Γ M[σ'τ'] M[σ'][τ'] : }}...
Qed.

@@ -933,22 +943,22 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i},
-    {{ Ψ A : Type@i }} ->
-    {{ Ψ M : A }} ->
-    {{ Δ s σ : Ψ }} ->
-    {{ Δ' s σ' : Ψ }} ->
-    {{ Γ s τ : Δ }} ->
-    {{ Γ s τ' : Δ' }} ->
-    {{ Γ s στ σ'τ' : Ψ }} ->
-    {{ Γ M[σ][τ] M[σ'][τ'] : A[στ] }}.
+Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i},
+    {{ Ψ A : Type@i }} ->
+    {{ Ψ M : A }} ->
+    {{ Δ s σ : Ψ }} ->
+    {{ Δ' s σ' : Ψ }} ->
+    {{ Γ s τ : Δ }} ->
+    {{ Γ s τ' : Δ' }} ->
+    {{ Γ s στ σ'τ' : Ψ }} ->
+    {{ Γ M[σ][τ] M[σ'][τ'] : A[στ] }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ A[στ] A[σ'τ'] : Type@i }} by mauto.
-  assert {{ Γ M[σ][τ] M[στ] : A[στ] }} by mauto.
-  assert {{ Γ M[στ] M[σ'τ'] : A[στ] }} by mauto.
-  assert {{ Γ M[σ'τ'] M[σ'][τ'] : A[σ'τ'] }} by mauto.
-  enough {{ Γ M[σ'τ'] M[σ'][τ'] : A[στ] }} by mauto.
+  assert {{ Γ A[στ] A[σ'τ'] : Type@i }} by mauto.
+  assert {{ Γ M[σ][τ] M[στ] : A[στ] }} by mauto.
+  assert {{ Γ M[στ] M[σ'τ'] : A[στ] }} by mauto.
+  assert {{ Γ M[σ'τ'] M[σ'][τ'] : A[σ'τ'] }} by mauto.
+  enough {{ Γ M[σ'τ'] M[σ'][τ'] : A[στ] }} by mauto.
  eapply wf_exp_eq_conv...
Qed.
@@ -957,13 +967,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_sub_sub_compose_cong : mcltt.

-Lemma ctxeq_ctx_lookup : forall {Γ Δ A x},
-    {{ Γ Δ }} ->
-    {{ #x : A Γ }} ->
-    exists B i,
-      {{ #x : B Δ }} /\
-        {{ Γ A B : Type@i }} /\
-        {{ Δ A B : Type@i }}.
+Lemma ctxeq_ctx_lookup : forall {Γ Δ A x},
+    {{ Γ Δ }} ->
+    {{ #x : A Γ }} ->
+    exists B i,
+      {{ #x : B Δ }} /\
+        {{ Γ A B : Type@i }} /\
+        {{ Δ A B : Type@i }}.
Proof with mautosolve.
  intros * HΓΔ Hx; gen Δ.
  induction Hx as [|* ? IHHx]; inversion_clear 1 as [|? ? ? ? ? HΓΔ'];
@@ -975,10 +985,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve ctxeq_ctx_lookup : mcltt.

-Lemma sub_id_on_typ : forall {Γ M A i},
-    {{ Γ A : Type@i }} ->
-    {{ Γ M : A }} ->
-    {{ Γ M : A[Id] }}.
+Lemma sub_id_on_typ : forall {Γ M A i},
+    {{ Γ A : Type@i }} ->
+    {{ Γ M : A }} ->
+    {{ Γ M : A[Id] }}.
Proof with mautosolve 4.
  intros.
  eapply wf_conv...
@@ -989,10 +999,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_id_on_typ : mcltt.

-Lemma sub_id_extend : forall {Γ M A i},
-    {{ Γ A : Type@i }} ->
-    {{ Γ M : A }} ->
-    {{ Γ s Id,,M : Γ, A }}.
+Lemma sub_id_extend : forall {Γ M A i},
+    {{ Γ A : Type@i }} ->
+    {{ Γ M : A }} ->
+    {{ Γ s Id,,M : Γ, A }}.
Proof with mautosolve 4.
  intros.
  econstructor...
@@ -1003,10 +1013,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_id_extend : mcltt.

-Lemma sub_eq_p_id_extend : forall {Γ M A i},
-    {{ Γ A : Type@i }} ->
-    {{ Γ M : A }} ->
-    {{ Γ s Wk (Id,,M) Id : Γ }}.
+Lemma sub_eq_p_id_extend : forall {Γ M A i},
+    {{ Γ A : Type@i }} ->
+    {{ Γ M : A }} ->
+    {{ Γ s Wk (Id,,M) Id : Γ }}.
Proof with mautosolve 4.
  intros.
  econstructor...
@@ -1019,43 +1029,43 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Rewrite -> @sub_eq_p_id_extend using mauto 4 : mcltt.

-Lemma sub_q : forall {Γ A i σ Δ},
-    {{ Δ A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, A[σ] s q σ : Δ, A }}.
+Lemma sub_q : forall {Γ A i σ Δ},
+    {{ Δ A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, A[σ] s q σ : Δ, A }}.
Proof with mautosolve 3.
  intros.
-  assert {{ Γ A[σ] : Type@i }} by mauto 4.
-  assert {{ Γ, A[σ] s Wk : Γ }} by mauto 4.
-  assert {{ Γ, A[σ] # 0 : A[σ][Wk] }} by mauto 4.
+  assert {{ Γ A[σ] : Type@i }} by mauto 4.
+  assert {{ Γ, A[σ] s Wk : Γ }} by mauto 4.
+  assert {{ Γ, A[σ] # 0 : A[σ][Wk] }} by mauto 4.
  econstructor; mauto 3.
  eapply wf_conv...
Qed.

-Lemma sub_q_typ : forall {Γ σ Δ i},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, Type@i s q σ : Δ, Type@i }}.
+Lemma sub_q_typ : forall {Γ σ Δ i},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, Type@i s q σ : Δ, Type@i }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ }} by mauto 3.
-  assert {{ Γ, Type@i s Wk : Γ }} by mauto 4.
-  assert {{ Γ, Type@i s σ Wk : Δ }} by mauto 4.
-  assert {{ Γ, Type@i # 0 : Type@i[Wk] }} by mauto 4.
-  assert {{ Γ, Type@i # 0 : Type@i }}...
+  assert {{ Γ }} by mauto 3.
+  assert {{ Γ, Type@i s Wk : Γ }} by mauto 4.
+  assert {{ Γ, Type@i s σ Wk : Δ }} by mauto 4.
+  assert {{ Γ, Type@i # 0 : Type@i[Wk] }} by mauto 4.
+  assert {{ Γ, Type@i # 0 : Type@i }}...
Qed.

-Lemma sub_q_nat : forall {Γ σ Δ},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, s q σ : Δ, }}.
+Lemma sub_q_nat : forall {Γ σ Δ},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, s q σ : Δ, }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ }} by mauto 3.
-  assert {{ Γ, s Wk : Γ }} by mauto 4.
-  assert {{ Γ, s σ Wk : Δ }} by mauto 4.
-  assert {{ Γ, # 0 : [Wk] }} by mauto 4.
-  assert {{ Γ, # 0 : }}...
+  assert {{ Γ }} by mauto 3.
+  assert {{ Γ, s Wk : Γ }} by mauto 4.
+  assert {{ Γ, s σ Wk : Δ }} by mauto 4.
+  assert {{ Γ, # 0 : [Wk] }} by mauto 4.
+  assert {{ Γ, # 0 : }}...
Qed.

@@ -1063,25 +1073,25 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_q sub_q_typ sub_q_nat : mcltt.

-Lemma exp_eq_var_1_sub_q_sigma_nat : forall {Γ A i σ Δ},
-    {{ Δ, A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, , A[q σ] #1[q (q σ)] #1 : }}.
+Lemma exp_eq_var_1_sub_q_sigma_nat : forall {Γ A i σ Δ},
+    {{ Δ, A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, , A[q σ] #1[q (q σ)] #1 : }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ, s q σ : Δ, }} by mauto.
-  assert {{ Γ, , A[q σ] }} by mauto 3.
-  assert {{ Δ, #0 : }} by mauto.
-  assert {{ Γ, , A[q σ] #0 : A[q σ][Wk] }} by mauto 4.
-  assert {{ Γ, , A[q σ] A[q σWk] A[q σ][Wk] : Type@i }} by mauto 4.
-  assert {{ Γ, , A[q σ] #0 : A[q σWk] }} by (eapply wf_conv; mauto 4).
-  assert {{ Γ, , A[q σ] s q σWk : Δ, }} by mauto 4.
-  assert {{ Γ, , A[q σ] #1[q (q σ)] #0[q σWk] : }} by mauto 4.
-  assert {{ Γ, , A[q σ] #0[q σWk] #0[q σ][Wk] : }} by mauto 4.
-  assert {{ Γ, s σWk : Δ }} by mauto 4.
-  assert {{ Γ, #0 : [σWk] }} by (eapply wf_conv; mauto 4).
-  assert {{ Γ, #0[q σ] #0 : }} by mauto 4.
-  assert {{ Γ, , A[q σ] #0[q σ][Wk] #0[Wk] : }} by mauto 4.
+  assert {{ Γ, s q σ : Δ, }} by mauto.
+  assert {{ Γ, , A[q σ] }} by mauto 3.
+  assert {{ Δ, #0 : }} by mauto.
+  assert {{ Γ, , A[q σ] #0 : A[q σ][Wk] }} by mauto 4.
+  assert {{ Γ, , A[q σ] A[q σWk] A[q σ][Wk] : Type@i }} by mauto 4.
+  assert {{ Γ, , A[q σ] #0 : A[q σWk] }} by (eapply wf_conv; mauto 4).
+  assert {{ Γ, , A[q σ] s q σWk : Δ, }} by mauto 4.
+  assert {{ Γ, , A[q σ] #1[q (q σ)] #0[q σWk] : }} by mauto 4.
+  assert {{ Γ, , A[q σ] #0[q σWk] #0[q σ][Wk] : }} by mauto 4.
+  assert {{ Γ, s σWk : Δ }} by mauto 4.
+  assert {{ Γ, #0 : [σWk] }} by (eapply wf_conv; mauto 4).
+  assert {{ Γ, #0[q σ] #0 : }} by mauto 4.
+  assert {{ Γ, , A[q σ] #0[q σ][Wk] #0[Wk] : }} by mauto 4.
  econstructor...
Qed.
@@ -1090,48 +1100,48 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_eq_var_1_sub_q_sigma_nat : mcltt.

-Lemma sub_id_extend_zero : forall {Γ},
-    {{ Γ }} ->
-    {{ Γ s Id,,zero : Γ, }}.
+Lemma sub_id_extend_zero : forall {Γ},
+    {{ Γ }} ->
+    {{ Γ s Id,,zero : Γ, }}.
Proof. mauto. Qed.

-Lemma sub_weak_compose_weak_extend_succ_var_1 : forall {Γ A i},
-    {{ Γ, A : Type@i }} ->
-    {{ Γ, , A s (Wk Wk),,succ #1 : Γ, }}.
+Lemma sub_weak_compose_weak_extend_succ_var_1 : forall {Γ A i},
+    {{ Γ, A : Type@i }} ->
+    {{ Γ, , A s (Wk Wk),,succ #1 : Γ, }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ, , A s Wk : Γ, }} by mauto 4.
-  enough {{ Γ, , A s Wk Wk : Γ }}...
+  assert {{ Γ, , A s Wk : Γ, }} by mauto 4.
+  enough {{ Γ, , A s Wk Wk : Γ }}...
Qed.

-Lemma sub_eq_id_extend_nat_compose_sigma : forall {Γ M σ Δ},
-    {{ Γ s σ : Δ }} ->
-    {{ Δ M : }} ->
-    {{ Γ s (Id,,M) σ σ,,M[σ] : Δ, }}.
+Lemma sub_eq_id_extend_nat_compose_sigma : forall {Γ M σ Δ},
+    {{ Γ s σ : Δ }} ->
+    {{ Δ M : }} ->
+    {{ Γ s (Id,,M) σ σ,,M[σ] : Δ, }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ s (Id,,M) σ (Id σ),,M[σ] : Δ, }} by mauto 4.
-  enough {{ Γ s (Id σ),,M[σ] σ,,M[σ] : Δ, }} by mauto 4.
+  assert {{ Γ s (Id,,M) σ (Id σ),,M[σ] : Δ, }} by mauto 4.
+  enough {{ Γ s (Id σ),,M[σ] σ,,M[σ] : Δ, }} by mauto 4.
  eapply sub_eq_extend_cong_nat...
Qed.

-Lemma sub_eq_id_extend_compose_sigma : forall {Γ M A σ Δ i},
-    {{ Γ s σ : Δ }} ->
-    {{ Δ A : Type@i }} ->
-    {{ Δ M : A }} ->
-    {{ Γ s (Id,,M) σ σ,,M[σ] : Δ, A }}.
+Lemma sub_eq_id_extend_compose_sigma : forall {Γ M A σ Δ i},
+    {{ Γ s σ : Δ }} ->
+    {{ Δ A : Type@i }} ->
+    {{ Δ M : A }} ->
+    {{ Γ s (Id,,M) σ σ,,M[σ] : Δ, A }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Δ s Id : Δ }} by mauto.
-  assert {{ Δ M : A[Id] }} by mauto.
-  assert {{ Γ s (Id,,M) σ (Id σ),,M[σ] : Δ, A }} by mauto 3.
-  assert {{ Γ M[σ] : A[Id][σ] }} by mauto.
-  assert {{ Γ A[Id][σ] A[Idσ] : Type@i }} by mauto.
-  assert {{ Γ M[σ] : A[Idσ] }} by mauto 4.
-  enough {{ Γ M[σ] M[σ] : A[Idσ] }}...
+  assert {{ Δ s Id : Δ }} by mauto.
+  assert {{ Δ M : A[Id] }} by mauto.
+  assert {{ Γ s (Id,,M) σ (Id σ),,M[σ] : Δ, A }} by mauto 3.
+  assert {{ Γ M[σ] : A[Id][σ] }} by mauto.
+  assert {{ Γ A[Id][σ] A[Idσ] : Type@i }} by mauto.
+  assert {{ Γ M[σ] : A[Idσ] }} by mauto 4.
+  enough {{ Γ M[σ] M[σ] : A[Idσ] }}...
Qed.

@@ -1139,17 +1149,17 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_id_extend_zero sub_weak_compose_weak_extend_succ_var_1 sub_eq_id_extend_nat_compose_sigma sub_eq_id_extend_compose_sigma : mcltt.

-Lemma sub_eq_sigma_compose_weak_id_extend : forall {Γ M A i σ Δ},
-    {{ Γ A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : A }} ->
-    {{ Γ s (σ Wk) (Id,,M) σ : Δ }}.
+Lemma sub_eq_sigma_compose_weak_id_extend : forall {Γ M A i σ Δ},
+    {{ Γ A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : A }} ->
+    {{ Γ s (σ Wk) (Id,,M) σ : Δ }}.
Proof with mautosolve.
  intros.
-  assert {{ Γ s Id,,M : Γ, A }} by mauto.
-  assert {{ Γ s (σ Wk) (Id,,M) σ (Wk (Id,,M)) : Δ }} by mauto 4.
-  assert {{ Γ s Wk (Id,,M) Id : Γ }} by mauto.
-  enough {{ Γ s σ (Wk (Id,,M)) σ Id : Δ }} by mauto.
+  assert {{ Γ s Id,,M : Γ, A }} by mauto.
+  assert {{ Γ s (σ Wk) (Id,,M) σ (Wk (Id,,M)) : Δ }} by mauto 4.
+  assert {{ Γ s Wk (Id,,M) Id : Γ }} by mauto.
+  enough {{ Γ s σ (Wk (Id,,M)) σ Id : Δ }} by mauto.
  econstructor...
Qed.
@@ -1158,26 +1168,26 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_sigma_compose_weak_id_extend : mcltt.

-Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ},
-    {{ Δ A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ M : A[σ] }} ->
-    {{ Γ s q σ (Id,,M) σ,,M : Δ, A }}.
+Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ},
+    {{ Δ A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ M : A[σ] }} ->
+    {{ Γ s q σ (Id,,M) σ,,M : Δ, A }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ }} by mauto 3.
-  assert {{ Γ A[σ] : Type@i }} by mauto.
-  assert {{ Γ M : A[σ] }} by mauto.
-  assert {{ Γ s Id,,M : Γ, A[σ] }} by mauto.
-  assert {{ Γ, A[σ] s Wk : Γ }} by mauto.
-  assert {{ Γ, A[σ] #0 : A[σ][Wk] }} by mauto.
-  assert {{ Γ, A[σ] #0 : A[σWk] }} by (eapply wf_conv; mauto 3).
-  assert {{ Γ s q σ (Id,,M) ((σ Wk) (Id,,M)),,#0[Id,,M] : Δ, A }} by mauto.
-  assert {{ Γ s (σ Wk) (Id,,M) σ : Δ }} by mauto.
-  assert {{ Γ M : A[σ][Id] }} by mauto 4.
-  assert {{ Γ #0[Id,,M] M : A[σ][Id] }} by mauto 3.
-  assert {{ Γ #0[Id,,M] M : A[σ] }} by mauto.
-  enough {{ Γ #0[Id,,M] M : A[(σ Wk) (Id,,M)] }} by mauto.
+  assert {{ Γ }} by mauto 3.
+  assert {{ Γ A[σ] : Type@i }} by mauto.
+  assert {{ Γ M : A[σ] }} by mauto.
+  assert {{ Γ s Id,,M : Γ, A[σ] }} by mauto.
+  assert {{ Γ, A[σ] s Wk : Γ }} by mauto.
+  assert {{ Γ, A[σ] #0 : A[σ][Wk] }} by mauto.
+  assert {{ Γ, A[σ] #0 : A[σWk] }} by (eapply wf_conv; mauto 3).
+  assert {{ Γ s q σ (Id,,M) ((σ Wk) (Id,,M)),,#0[Id,,M] : Δ, A }} by mauto.
+  assert {{ Γ s (σ Wk) (Id,,M) σ : Δ }} by mauto.
+  assert {{ Γ M : A[σ][Id] }} by mauto 4.
+  assert {{ Γ #0[Id,,M] M : A[σ][Id] }} by mauto 3.
+  assert {{ Γ #0[Id,,M] M : A[σ] }} by mauto.
+  enough {{ Γ #0[Id,,M] M : A[(σ Wk) (Id,,M)] }} by mauto.
  eapply wf_exp_eq_conv...
Qed.
@@ -1188,15 +1198,15 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Rewrite -> @sub_eq_q_sigma_id_extend using mauto 4 : mcltt.

-Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ},
-    {{ Δ A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, A[σ] s Wk q σ σ Wk : Δ }}.
+Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ},
+    {{ Δ A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, A[σ] s Wk q σ σ Wk : Δ }}.
Proof with mautosolve 3.
  intros.
-  assert {{ Γ, A[σ] s Wk : Γ }} by mauto 4.
-  assert {{ Γ, A[σ] #0 : A[σ][Wk] }} by mauto 3.
-  enough {{ Γ, A[σ] #0 : A[σ Wk] }} by mauto.
+  assert {{ Γ, A[σ] s Wk : Γ }} by mauto 4.
+  assert {{ Γ, A[σ] #0 : A[σ][Wk] }} by mauto 3.
+  enough {{ Γ, A[σ] #0 : A[σ Wk] }} by mauto.
  eapply wf_conv...
Qed.
@@ -1205,12 +1215,12 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_p_q_sigma : mcltt.

-Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ},
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, s Wk q σ σ Wk : Δ }}.
+Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ},
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, s Wk q σ σ Wk : Δ }}.
Proof with mautosolve.
  intros.
-  assert {{ Γ, #0 : }}...
+  assert {{ Γ, #0 : }}...
Qed.

@@ -1218,22 +1228,22 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_p_q_sigma_nat : mcltt.

-Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ},
-    {{ Δ, A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, , A[q σ] s Wk (Wk q (q σ)) (σ Wk) Wk : Δ }}.
+Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ},
+    {{ Δ, A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, , A[q σ] s Wk (Wk q (q σ)) (σ Wk) Wk : Δ }}.
Proof with mautosolve 3.
  intros.
-  assert {{ Γ, A[q σ] : Type@i }} by mauto.
-  assert {{ Γ, , A[q σ] }} by mauto 3.
-  assert {{ Δ, }} by mauto 3.
-  assert {{ Γ, , A[q σ] s Wkq (q σ) q σ Wk : Δ, }} by mauto.
-  assert {{ Γ, , A[q σ] s Wk(Wkq (q σ)) Wk (q σ Wk) : Δ }} by mauto 3.
-  assert {{ Δ, s Wk : Δ }} by mauto.
-  assert {{ Γ, s q σ : Δ, }} by mauto.
-  assert {{ Γ, , A[q σ] s Wk (q σ Wk) (Wk q σ) Wk : Δ }} by mauto 4.
-  assert {{ Γ, s Wk q σ σ Wk : Δ }} by mauto.
-  enough {{ Γ, , A[q σ] s (Wk q σ) Wk (σ Wk) Wk : Δ }}...
+  assert {{ Γ, A[q σ] : Type@i }} by mauto.
+  assert {{ Γ, , A[q σ] }} by mauto 3.
+  assert {{ Δ, }} by mauto 3.
+  assert {{ Γ, , A[q σ] s Wkq (q σ) q σ Wk : Δ, }} by mauto.
+  assert {{ Γ, , A[q σ] s Wk(Wkq (q σ)) Wk (q σ Wk) : Δ }} by mauto 3.
+  assert {{ Δ, s Wk : Δ }} by mauto.
+  assert {{ Γ, s q σ : Δ, }} by mauto.
+  assert {{ Γ, , A[q σ] s Wk (q σ Wk) (Wk q σ) Wk : Δ }} by mauto 4.
+  assert {{ Γ, s Wk q σ σ Wk : Δ }} by mauto.
+  enough {{ Γ, , A[q σ] s (Wk q σ) Wk (σ Wk) Wk : Δ }}...
Qed.

@@ -1241,52 +1251,52 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve sub_eq_p_p_q_q_sigma_nat : mcltt.

-Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : forall {Γ A i σ Δ},
-    {{ Δ, A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, , A[q σ] s q σ ((Wk Wk),,succ #1) ((Wk Wk),,succ #1) q (q σ) : Δ, }}.
+Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : forall {Γ A i σ Δ},
+    {{ Δ, A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, , A[q σ] s q σ ((Wk Wk),,succ #1) ((Wk Wk),,succ #1) q (q σ) : Δ, }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Δ, , A }} by mauto 3.
-  assert {{ Γ, }} by mauto 3.
-  assert {{ Γ, s Wk : Γ }} by mauto 3.
-  assert {{ Γ, s σWk : Δ }} by mauto 3.
-  assert {{ Γ, A[q σ] : Type@i }} by mauto 3.
-  set (Γ' := {{{ Γ, , A[q σ] }}}).
+  assert {{ Δ, , A }} by mauto 3.
+  assert {{ Γ, }} by mauto 3.
+  assert {{ Γ, s Wk : Γ }} by mauto 3.
+  assert {{ Γ, s σWk : Δ }} by mauto 3.
+  assert {{ Γ, A[q σ] : Type@i }} by mauto 3.
+  set (Γ' := {{{ Γ, , A[q σ] }}}).
  set (WkWksucc := {{{ (WkWk),,succ #1 }}}).
-  assert {{ Γ' }} by mauto 2.
-  assert {{ Γ' s WkWk : Γ }} by mauto 4.
-  assert {{ Γ' s WkWksucc : Γ, }} by mauto.
-  assert {{ Γ, #0 : }} by mauto.
-  assert {{ Γ' s q σWkWksucc ((σWk)WkWksucc),,#0[WkWksucc] : Δ, }} by mautosolve 3.
-  assert {{ Γ' #1 : [Wk][Wk] }} by mauto.
-  assert {{ Γ' [Wk][Wk] : Type@0 }} by mauto 3.
-  assert {{ Γ' #1 : }} by mauto 2.
-  assert {{ Γ' succ #1 : }} by mauto.
-  assert {{ Γ' s WkWkWksucc : Γ }} by mauto 4.
-  assert {{ Γ' s WkWkWksucc WkWk : Γ }} by mauto 4.
-  assert {{ Γ s σ σ : Δ }} by mauto.
-  assert {{ Γ' s σ(WkWkWksucc) σ(WkWk) : Δ }} by mauto 3.
-  assert {{ Γ' s (σWk)WkWksucc σ(WkWk) : Δ }} by mauto 3.
-  assert {{ Γ' s σ(WkWk) (σWk)Wk : Δ }} by mauto 4.
-  assert {{ Γ' s (σWk)Wk Wk(Wkq (q σ)) : Δ }} by mauto.
-  assert {{ Δ, s Wk : Δ }} by mauto 4.
-  assert {{ Δ, , A s Wk : Δ, }} by mauto 4.
-  assert {{ Δ, , A s WkWk : Δ }} by mauto 4.
-  assert {{ Γ' s q (q σ) : Δ, , A }} by mauto.
-  assert {{ Γ' s Wk(Wkq (q σ)) (WkWk)q (q σ) : Δ }} by mauto 3.
-  assert {{ Γ' s σ(WkWk) (WkWk)q (q σ) : Δ }} by mauto 3.
-  assert {{ Γ' #0[WkWksucc] succ #1 : }} by mauto.
-  assert {{ Γ' succ #1[q (q σ)] succ #1 : }} by mauto 3.
-  assert {{ Δ, , A #1 : }} by mauto 2.
-  assert {{ Γ' succ #1 (succ #1)[q (q σ)] : }} by mauto 4.
-  assert {{ Γ' #0[WkWksucc] (succ #1)[q (q σ)] : }} by mauto 2.
-  assert {{ Γ' s (σWk)WkWksucc : Δ }} by mauto 3.
-  assert {{ Γ' s ((σWk)WkWksucc),,#0[WkWksucc] ((WkWk)q (q σ)),,(succ #1)[q (q σ)] : Δ, }} by mauto 3.
-  assert {{ Δ, , A #1 : [Wk][Wk] }} by mauto 4.
-  assert {{ Δ, , A [Wk][Wk] : Type@0 }} by mauto 3.
-  assert {{ Δ, , A succ #1 : }} by mauto.
-  enough {{ Γ' s ((WkWk)q (q σ)),,(succ #1)[q (q σ)] WkWksuccq (q σ) : Δ, }}...
+  assert {{ Γ' }} by mauto 2.
+  assert {{ Γ' s WkWk : Γ }} by mauto 4.
+  assert {{ Γ' s WkWksucc : Γ, }} by mauto.
+  assert {{ Γ, #0 : }} by mauto.
+  assert {{ Γ' s q σWkWksucc ((σWk)WkWksucc),,#0[WkWksucc] : Δ, }} by mautosolve 3.
+  assert {{ Γ' #1 : [Wk][Wk] }} by mauto.
+  assert {{ Γ' [Wk][Wk] : Type@0 }} by mauto 3.
+  assert {{ Γ' #1 : }} by mauto 2.
+  assert {{ Γ' succ #1 : }} by mauto.
+  assert {{ Γ' s WkWkWksucc : Γ }} by mauto 4.
+  assert {{ Γ' s WkWkWksucc WkWk : Γ }} by mauto 4.
+  assert {{ Γ s σ σ : Δ }} by mauto.
+  assert {{ Γ' s σ(WkWkWksucc) σ(WkWk) : Δ }} by mauto 3.
+  assert {{ Γ' s (σWk)WkWksucc σ(WkWk) : Δ }} by mauto 3.
+  assert {{ Γ' s σ(WkWk) (σWk)Wk : Δ }} by mauto 4.
+  assert {{ Γ' s (σWk)Wk Wk(Wkq (q σ)) : Δ }} by mauto.
+  assert {{ Δ, s Wk : Δ }} by mauto 4.
+  assert {{ Δ, , A s Wk : Δ, }} by mauto 4.
+  assert {{ Δ, , A s WkWk : Δ }} by mauto 4.
+  assert {{ Γ' s q (q σ) : Δ, , A }} by mauto.
+  assert {{ Γ' s Wk(Wkq (q σ)) (WkWk)q (q σ) : Δ }} by mauto 3.
+  assert {{ Γ' s σ(WkWk) (WkWk)q (q σ) : Δ }} by mauto 3.
+  assert {{ Γ' #0[WkWksucc] succ #1 : }} by mauto.
+  assert {{ Γ' succ #1[q (q σ)] succ #1 : }} by mauto 3.
+  assert {{ Δ, , A #1 : }} by mauto 2.
+  assert {{ Γ' succ #1 (succ #1)[q (q σ)] : }} by mauto 4.
+  assert {{ Γ' #0[WkWksucc] (succ #1)[q (q σ)] : }} by mauto 2.
+  assert {{ Γ' s (σWk)WkWksucc : Δ }} by mauto 3.
+  assert {{ Γ' s ((σWk)WkWksucc),,#0[WkWksucc] ((WkWk)q (q σ)),,(succ #1)[q (q σ)] : Δ, }} by mauto 3.
+  assert {{ Δ, , A #1 : [Wk][Wk] }} by mauto 4.
+  assert {{ Δ, , A [Wk][Wk] : Type@0 }} by mauto 3.
+  assert {{ Δ, , A succ #1 : }} by mauto.
+  enough {{ Γ' s ((WkWk)q (q σ)),,(succ #1)[q (q σ)] WkWksuccq (q σ) : Δ, }}...
Qed.

@@ -1303,9 +1313,9 @@

Mcltt.Core.Syntactic.System.Lemmas


-Fact wf_subtyp_refl : forall {Γ A i},
-    {{ Γ A : Type@i }} ->
-    {{ Γ A A }}.
+Fact wf_subtyp_refl : forall {Γ A i},
+    {{ Γ A : Type@i }} ->
+    {{ Γ A A }}.
Proof. mauto. Qed.

@@ -1313,10 +1323,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_subtyp_refl : mcltt.

-Lemma wf_subtyp_ge : forall {Γ i j},
-    {{ Γ }} ->
-    i <= j ->
-    {{ Γ Type@i Type@j }}.
+Lemma wf_subtyp_ge : forall {Γ i j},
+    {{ Γ }} ->
+    i <= j ->
+    {{ Γ Type@i Type@j }}.
Proof.
  induction 2; mauto 4.
Qed.
@@ -1326,18 +1336,18 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_subtyp_ge : mcltt.

-Lemma wf_subtyp_sub : forall {Δ A A'},
-    {{ Δ A A' }} ->
-    forall Γ σ,
-    {{ Γ s σ : Δ }} ->
-    {{ Γ A[σ] A'[σ] }}.
+Lemma wf_subtyp_sub : forall {Δ A A'},
+    {{ Δ A A' }} ->
+    forall Γ σ,
+    {{ Γ s σ : Δ }} ->
+    {{ Γ A[σ] A'[σ] }}.
Proof.
  induction 1; intros; mauto 4.
  - transitivity {{{ Type@i }}}; [econstructor; mauto 4 |].
    transitivity {{{ Type@j }}}; [| econstructor; mauto 4].
    mauto 3.
-  - transitivity {{{ Π (A[σ]) (B[q σ]) }}}; [econstructor; mauto |].
-    transitivity {{{ Π (A'[σ]) (B'[q σ]) }}}; [ | econstructor; mauto 4].
+  - transitivity {{{ Π (A[σ]) (B[q σ]) }}}; [econstructor; mauto |].
+    transitivity {{{ Π (A'[σ]) (B'[q σ]) }}}; [ | econstructor; mauto 4].
    eapply wf_subtyp_pi with (i := i); mauto 4.
Qed.
@@ -1346,10 +1356,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve wf_subtyp_sub : mcltt.

-Lemma wf_subtyp_univ_weaken : forall {Γ i j A},
-    {{ Γ Type@i Type@j }} ->
-    {{ Γ, A }} ->
-    {{ Γ, A Type@i Type@j }}.
+Lemma wf_subtyp_univ_weaken : forall {Γ i j A},
+    {{ Γ Type@i Type@j }} ->
+    {{ Γ, A }} ->
+    {{ Γ, A Type@i Type@j }}.
Proof.
  intros.
  eapply wf_subtyp_sub with (σ := {{{ Wk }}}) in H.
@@ -1359,13 +1369,13 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma ctx_sub_ctx_lookup : forall {Γ Δ},
-    {{ Δ Γ }} ->
-    forall {A x},
-      {{ #x : A Γ }} ->
-      exists B,
-        {{ #x : B Δ }} /\
-          {{ Δ B A }}.
+Lemma ctx_sub_ctx_lookup : forall {Γ Δ},
+    {{ Δ Γ }} ->
+    forall {A x},
+      {{ #x : A Γ }} ->
+      exists B,
+        {{ #x : B Δ }} /\
+          {{ Δ B A }}.
Proof with (do 2 eexists; repeat split; mautosolve).
  induction 1; intros * Hx; progressive_inversion.
  dependent destruction Hx.
@@ -1378,34 +1388,34 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve ctx_sub_ctx_lookup : mcltt.

-Lemma sub_lookup_var0 : forall Δ Γ σ M1 M2 B i,
-    {{Δ s σ : Γ}} ->
-    {{Γ B : Type@i}} ->
-    {{Δ M1 : B[σ]}} ->
-    {{Δ M2 : B[σ]}} ->
-    {{Δ #0[σ,,M1,,M2] M2 : B[σ]}}.
+Lemma sub_lookup_var0 : forall Δ Γ σ M1 M2 B i,
+    {{Δ s σ : Γ}} ->
+    {{Γ B : Type@i}} ->
+    {{Δ M1 : B[σ]}} ->
+    {{Δ M2 : B[σ]}} ->
+    {{Δ #0[σ,,M1,,M2] M2 : B[σ]}}.
Proof.
  intros.
-  assert {{ Γ , B B[Wk] : Type@i }} by mauto.
-  assert {{ Δ s σ ,, M1 : Γ, B}} by mauto 4.
-  assert {{ Δ B[Wk][σ,,M1] : Type @ i }} by mauto 4.
-  assert {{ Δ B[Wk][σ,,M1] B[σ] : Type @ i }}.
+  assert {{ Γ , B B[Wk] : Type@i }} by mauto.
+  assert {{ Δ s σ ,, M1 : Γ, B}} by mauto 4.
+  assert {{ Δ B[Wk][σ,,M1] : Type @ i }} by mauto 4.
+  assert {{ Δ B[Wk][σ,,M1] B[σ] : Type @ i }}.
  {
-    transitivity {{{B[Wk (σ,,M1)]}}}.
+    transitivity {{{B[Wk (σ,,M1)]}}}.
    - eapply exp_eq_sub_compose_typ; mauto 4.
    - eapply exp_eq_sub_cong_typ2'; mauto 4.
  }
  eapply wf_exp_eq_conv;
-    [eapply wf_exp_eq_var_0_sub with (A := {{{B[Wk]}}}) | |];
+    [eapply wf_exp_eq_var_0_sub with (A := {{{B[Wk]}}}) | |];
    mauto 4.
Qed.

-Lemma id_sub_lookup_var0 : forall Γ M1 M2 B i,
-    {{Γ B : Type@i}} ->
-    {{Γ M1 : B}} ->
-    {{Γ M2 : B}} ->
-    {{Γ #0[Id,,M1,,M2] M2 : B}}.
+Lemma id_sub_lookup_var0 : forall Γ M1 M2 B i,
+    {{Γ B : Type@i}} ->
+    {{Γ M1 : B}} ->
+    {{Γ M2 : B}} ->
+    {{Γ #0[Id,,M1,,M2] M2 : B}}.
Proof.
  intros.
  eapply wf_exp_eq_conv;
@@ -1414,24 +1424,24 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma sub_lookup_var1 : forall Δ Γ σ M1 M2 B i,
-    {{Δ s σ : Γ}} ->
-    {{Γ B : Type@i}} ->
-    {{Δ M1 : B[σ]}} ->
-    {{Δ M2 : B[σ]}} ->
-    {{Δ #1[σ,,M1,,M2] M1 : B[σ]}}.
+Lemma sub_lookup_var1 : forall Δ Γ σ M1 M2 B i,
+    {{Δ s σ : Γ}} ->
+    {{Γ B : Type@i}} ->
+    {{Δ M1 : B[σ]}} ->
+    {{Δ M2 : B[σ]}} ->
+    {{Δ #1[σ,,M1,,M2] M1 : B[σ]}}.
Proof.
  intros.
-  assert {{ Γ , B B[Wk] : Type@i }} by mauto.
-  assert {{ Δ s σ ,, M1 : Γ, B}} by mauto 4.
-  assert {{ Δ B[Wk][σ,,M1] : Type @ i }} by mauto 4.
-  assert {{ Δ B[Wk][σ,,M1] B[σ] : Type @ i }}.
+  assert {{ Γ , B B[Wk] : Type@i }} by mauto.
+  assert {{ Δ s σ ,, M1 : Γ, B}} by mauto 4.
+  assert {{ Δ B[Wk][σ,,M1] : Type @ i }} by mauto 4.
+  assert {{ Δ B[Wk][σ,,M1] B[σ] : Type @ i }}.
  {
-    transitivity {{{B[Wk (σ,,M1)]}}}.
+    transitivity {{{B[Wk (σ,,M1)]}}}.
    - eapply exp_eq_sub_compose_typ; mauto 4.
    - eapply exp_eq_sub_cong_typ2'; mauto 4.
  }
-  transitivity {{{#0[σ,,M1]}}}.
+  transitivity {{{#0[σ,,M1]}}}.
  - eapply wf_exp_eq_conv;
      [eapply wf_exp_eq_var_S_sub | |];
      mauto 4.
@@ -1442,11 +1452,11 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma id_sub_lookup_var1 : forall Γ M1 M2 B i,
-    {{Γ B : Type@i}} ->
-    {{Γ M1 : B}} ->
-    {{Γ M2 : B}} ->
-    {{Γ #1[Id,,M1,,M2] M1 : B}}.
+Lemma id_sub_lookup_var1 : forall Γ M1 M2 B i,
+    {{Γ B : Type@i}} ->
+    {{Γ M1 : B}} ->
+    {{Γ M2 : B}} ->
+    {{Γ #1[Id,,M1,,M2] M1 : B}}.
Proof.
  intros.
  eapply wf_exp_eq_conv;
@@ -1455,55 +1465,55 @@

Mcltt.Core.Syntactic.System.Lemmas

Qed.

-Lemma exp_eq_var_1_sub_q_sigma : forall {Γ A i B j σ Δ},
-    {{ Δ B : Type@j }} ->
-    {{ Δ, B A : Type@i }} ->
-    {{ Γ s σ : Δ }} ->
-    {{ Γ, B[σ], A[q σ] #1[q (q σ)] #1 : B[σ][Wk][Wk] }}.
+Lemma exp_eq_var_1_sub_q_sigma : forall {Γ A i B j σ Δ},
+    {{ Δ B : Type@j }} ->
+    {{ Δ, B A : Type@i }} ->
+    {{ Γ s σ : Δ }} ->
+    {{ Γ, B[σ], A[q σ] #1[q (q σ)] #1 : B[σ][Wk][Wk] }}.
Proof with mautosolve 4.
  intros.
-  assert {{ Γ, B[σ] s q σ : Δ, B }} by mauto.
-  assert {{ Γ, B[σ], A[q σ] }} by mauto 3.
-  assert {{ Δ, B B[Wk] : Type@j }} by mauto.
-  assert {{ Δ, B #0 : B[Wk] }} by mauto.
-  assert {{ Γ, B[σ], A[q σ] #0 : A[q σ][Wk] }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] A[q σWk] A[q σ][Wk] : Type@i }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] #0 : A[q σWk] }} by (eapply wf_conv; mauto 4).
-  assert {{ Γ, B[σ], A[q σ] s q σWk : Δ, B }} by mauto 4.
-  assert {{ Γ B[σ] : Type@j }} by mauto 3.
-  assert {{ Γ,B[σ] B[σ][Wk] : Type@j }} by mauto 4.
-  assert {{Γ, B[σ], A[q σ] B[σ][Wk][Wk] : Type@j}} by mauto 4.
-  assert {{Γ, B[σ],A[q σ] B[Wk][q σ Wk] : Type@j}} by mauto.
-  assert {{Γ, B[σ] B[Wk][q σ] B[σ][Wk] : Type@j}}.
+  assert {{ Γ, B[σ] s q σ : Δ, B }} by mauto.
+  assert {{ Γ, B[σ], A[q σ] }} by mauto 3.
+  assert {{ Δ, B B[Wk] : Type@j }} by mauto.
+  assert {{ Δ, B #0 : B[Wk] }} by mauto.
+  assert {{ Γ, B[σ], A[q σ] #0 : A[q σ][Wk] }} by mauto 4.
+  assert {{ Γ, B[σ], A[q σ] A[q σWk] A[q σ][Wk] : Type@i }} by mauto 4.
+  assert {{ Γ, B[σ], A[q σ] #0 : A[q σWk] }} by (eapply wf_conv; mauto 4).
+  assert {{ Γ, B[σ], A[q σ] s q σWk : Δ, B }} by mauto 4.
+  assert {{ Γ B[σ] : Type@j }} by mauto 3.
+  assert {{ Γ,B[σ] B[σ][Wk] : Type@j }} by mauto 4.
+  assert {{Γ, B[σ], A[q σ] B[σ][Wk][Wk] : Type@j}} by mauto 4.
+  assert {{Γ, B[σ],A[q σ] B[Wk][q σ Wk] : Type@j}} by mauto.
+  assert {{Γ, B[σ] B[Wk][q σ] B[σ][Wk] : Type@j}}.
  {
-    transitivity {{{B[Wk q σ]}}};
-      [mauto 4 | transitivity {{{B[σ Wk]}}}];
+    transitivity {{{B[Wk q σ]}}};
+      [mauto 4 | transitivity {{{B[σ Wk]}}}];
      [eapply exp_eq_sub_cong_typ2'; mauto 4 | mauto].
  }
-  assert {{Γ, B[σ],A[q σ] B[Wk][q σ Wk] B[σ][Wk][Wk] : Type@j}}.
+  assert {{Γ, B[σ],A[q σ] B[Wk][q σ Wk] B[σ][Wk][Wk] : Type@j}}.
  {
-    transitivity {{{B[Wk][q σ][Wk]}}};
+    transitivity {{{B[Wk][q σ][Wk]}}};
      [mauto 4 |].
    eapply exp_eq_sub_cong_typ1; mauto 3.
  }
-  assert {{ Γ, B[σ], A[q σ] #1[q (q σ)] #0[q σWk] : B[σ][Wk][Wk] }} by mauto 3.
-  assert {{ Γ, B[σ], A[q σ] #0[q σWk] #0[q σ][Wk] : B[σ][Wk][Wk] }} by mauto 4.
-  assert {{ Γ, B[σ] s σWk : Δ }} by mauto 4.
-  assert {{ Γ, B[σ] #0 : B[σWk] }}.
+  assert {{ Γ, B[σ], A[q σ] #1[q (q σ)] #0[q σWk] : B[σ][Wk][Wk] }} by mauto 3.
+  assert {{ Γ, B[σ], A[q σ] #0[q σWk] #0[q σ][Wk] : B[σ][Wk][Wk] }} by mauto 4.
+  assert {{ Γ, B[σ] s σWk : Δ }} by mauto 4.
+  assert {{ Γ, B[σ] #0 : B[σWk] }}.
  {
-    eapply wf_conv with (A:={{{B[σ][Wk]}}}); mauto 2; mauto 4.
+    eapply wf_conv with (A:={{{B[σ][Wk]}}}); mauto 2; mauto 4.
  }
-  assert {{ Γ, B[σ] #0[q σ] #0 : B[σ Wk] }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] #0[q σ][Wk] #0[Wk] : B[σ Wk][Wk] }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] B[σ Wk][Wk] B[σ][Wk][Wk] : Type@j}}.
+  assert {{ Γ, B[σ] #0[q σ] #0 : B[σ Wk] }} by mauto 4.
+  assert {{ Γ, B[σ], A[q σ] #0[q σ][Wk] #0[Wk] : B[σ Wk][Wk] }} by mauto 4.
+  assert {{ Γ, B[σ], A[q σ] B[σ Wk][Wk] B[σ][Wk][Wk] : Type@j}}.
  {
    eapply exp_eq_sub_cong_typ1; mauto 3.
    symmetry.
    mauto 4.
  }
-  assert {{ Γ, B[σ], A[q σ] #0[q σ][Wk] #0[Wk] : B[σ][Wk][Wk] }} by mauto 4.
+  assert {{ Γ, B[σ], A[q σ] #0[q σ][Wk] #0[Wk] : B[σ][Wk][Wk] }} by mauto 4.
  etransitivity; mauto 2.
-  transitivity {{{#0[q σ][Wk]}}}; mauto 3.
+  transitivity {{{#0[q σ][Wk]}}}; mauto 3.
Qed.

@@ -1516,48 +1526,62 @@

Mcltt.Core.Syntactic.System.Lemmas


-Lemma presup_exp_typ : forall {Γ M A},
-    {{ Γ M : A }} ->
-    exists i, {{ Γ A : Type@i }}.
+Lemma presup_exp_typ : forall {Γ M A},
+    {{ Γ M : A }} ->
+    exists i, {{ Γ A : Type@i }}.
Proof.
-  induction 1; assert {{ Γ }} by mauto 3; destruct_conjs; mauto 3.
-  - enough {{ Γ s Id,,M : Γ, }}; mauto 3.
+  induction 1; assert {{ Γ }} by mauto 3; destruct_conjs; mauto 3.
+  - enough {{ Γ s Id,,M : Γ, }}; mauto 3.
  - eexists; mauto 4 using lift_exp_max_left, lift_exp_max_right.
-  - enough {{ Γ s Id,,N : Γ, A }}; mauto 3.
-  - assert {{ Γ s Id,,M1 : Γ, A }} by mauto 3.
-    assert {{ Γ, A s Wk : Γ }} by mauto 3.
-    assert {{ Γ, A A[Wk] : Type@i }} by mauto 3.
-    assert {{ Γ, A, A[Wk] s Wk : Γ, A }} by mauto 4.
-    assert {{ Γ, A, A[Wk] A[Wk][Wk] : Type@i }} by mauto 3.
-    assert {{ Γ A[Wk][Id,,M1] : Type@i }} by mauto 3.
-    assert {{ Γ A[Wk][Id,,M1] A : Type@i }}.
+  - enough {{ Γ s Id,,N : Γ, A }}; mauto 3.
+  - assert {{ Γ s Id,,M1 : Γ, A }} by mauto 3.
+    assert {{ Γ, A s Wk : Γ }} by mauto 3.
+    assert {{ Γ, A A[Wk] : Type@i }} by mauto 3.
+    assert {{ Γ, A, A[Wk] s Wk : Γ, A }} by mauto 4.
+    assert {{ Γ, A, A[Wk] A[Wk][Wk] : Type@i }} by mauto 3.
+    assert {{ Γ A[Wk][Id,,M1] : Type@i }} by mauto 3.
+    assert {{ Γ A[Wk][Id,,M1] A : Type@i }}.
    {
-      transitivity {{{ A[Wk(Id,,M1)] }}}; mauto 3.
-      transitivity {{{ A[Id] }}}; mauto 4.
+      transitivity {{{ A[Wk(Id,,M1)] }}}; mauto 3.
+      transitivity {{{ A[Id] }}}; mauto 4.
    }
-    assert {{ Γ s Id,,M1,,M2 : Γ, A, A[Wk] }} by mauto 4.
-    assert {{ Γ A[Wk][Wk][Id ,, M1 ,, M2] A : Type@i }}.
+    assert {{ Γ s Id,,M1,,M2 : Γ, A, A[Wk] }} by mauto 4.
+    assert {{ Γ A[Wk][Wk][Id ,, M1 ,, M2] A : Type@i }}.
    {
-      transitivity {{{ A[Wk][Wk(Id,,M1,,M2)] }}}; mauto 3.
-      transitivity {{{ A[Wk][Id,,M1] }}}; mauto 3.
+      transitivity {{{ A[Wk][Wk(Id,,M1,,M2)] }}}; mauto 3.
+      transitivity {{{ A[Wk][Id,,M1] }}}; mauto 3.
      eapply exp_eq_sub_cong_typ2'; mauto 4.
    }
-    enough {{ Γ s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk][Wk] #1 #0 }} by mauto 3.
-    assert {{ Γ, A, A[Wk] Eq A[Wk][Wk] #1 #0 : Type@i }} by (econstructor; mauto 4).
+    enough {{ Γ s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk][Wk] #1 #0 }} by mauto 3.
+    assert {{ Γ, A, A[Wk] Eq A[Wk][Wk] #1 #0 : Type@i }} by (econstructor; mauto 4).
    econstructor; mauto 3.
    eapply wf_conv; mauto 2.
-    transitivity {{{ Eq A[Wk][Wk][Id,,M1,,M2] #1[Id,,M1,,M2] #0[Id,,M1,,M2] }}}.
+    transitivity {{{ Eq A[Wk][Wk][Id,,M1,,M2] #1[Id,,M1,,M2] #0[Id,,M1,,M2] }}}.
    + econstructor; mauto 3 using id_sub_lookup_var0, id_sub_lookup_var1.
    + symmetry; econstructor; mauto 4.
Qed.

-Lemma presup_exp : forall {Γ M A},
-    {{ Γ M : A }} ->
-    {{ Γ }} /\ exists i, {{ Γ A : Type@i }}.
+Lemma presup_exp : forall {Γ M A},
+    {{ Γ M : A }} ->
+    {{ Γ }} /\ exists i, {{ Γ A : Type@i }}.
Proof.
  mauto 4 using presup_exp_typ.
Qed.
+ +
+Lemma no_closed_neutral : forall {A} {W : ne},
+    ~ {{ W : A }}.
+Proof.
+  intros * H.
+  dependent induction H; destruct W;
+    try (simpl in *; congruence);
+    autoinjections;
+    intuition.
+  inversion_by_head ctx_lookup.
+Qed.
+#[export]
+Hint Resolve no_closed_neutral : mcltt.