From 22cfcca1190660cfd2a0eab9d7647f1d7d01d7b9 Mon Sep 17 00:00:00 2001 From: Ailrun Date: Wed, 2 Oct 2024 03:29:28 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20Beluga-l?= =?UTF-8?q?ang/McLTT@27536203b3e85ff06abf74d36d94133758fb2ee0=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ....Core.Completeness.Consequences.Types.html | 77 +- Mcltt.Core.Semantic.Consequences.html | 184 ++- Mcltt.Core.Semantic.NbE.html | 95 +- Mcltt.Core.Syntactic.System.Lemmas.html | 1008 +++++++------- dep.html | 1166 +++++++++-------- indexpage.html | 50 +- 6 files changed, 1424 insertions(+), 1156 deletions(-) diff --git a/Mcltt.Core.Completeness.Consequences.Types.html b/Mcltt.Core.Completeness.Consequences.Types.html index 3f89e99..d1e194a 100644 --- a/Mcltt.Core.Completeness.Consequences.Types.html +++ b/Mcltt.Core.Completeness.Consequences.Types.html @@ -33,6 +33,7 @@

Mcltt.Core.Completeness.Consequences.Types

From Mcltt.Core Require Import Base.
From Mcltt.Core Require Export Completeness.
From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Syntactic Require Export CoreInversions.
Import Domain_Notations.

@@ -54,8 +55,6 @@

Mcltt.Core.Completeness.Consequences.Types

  match_by_head1 per_univ_elem invert_per_univ_elem.
  reflexivity.
Qed.
- -
#[export]
Hint Resolve exp_eq_typ_implies_eq_level : mcltt.
@@ -64,49 +63,89 @@

Mcltt.Core.Completeness.Consequences.Types

| typ_is_typ_constr : forall i, is_typ_constr {{{ Type@i }}}
| nat_is_typ_constr : is_typ_constr {{{ ℕ }}}
| pi_is_typ_constr : forall A B, is_typ_constr {{{ Π A B }}}
+| var_is_typ_constr : forall x, is_typ_constr {{{ #x }}}
.
- -
#[export]
Hint Constructors is_typ_constr : mcltt.

-Theorem is_typ_constr_and_exp_eq_typ_implies_eq_typ : forall Γ A i j,
-    is_typ_constr A ->
-    {{ Γ ⊢ A ≈ Type@i : Type@j }} ->
-    A = {{{ Type@i }}}.
+Theorem is_typ_constr_and_exp_eq_var_implies_eq_var : forall Γ A x i,
+    is_typ_constr A ->
+    {{ Γ ⊢ A ≈ #x : Type@i }} ->
+    A = {{{ #x }}}.
Proof.
  intros * Histyp ?.
-  assert {{ Γ ⊨ A ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  assert {{ Γ ⊨ A ≈ #x : Type@i }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
  destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
  destruct_conjs.
  functional_initial_env_rewrite_clear.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
  destruct_by_head rel_typ.
  invert_rel_typ_body.
  destruct_by_head rel_exp.
+  gen_presups.
+  assert (exists A, {{ #x : A ∈ Γ }} /\ {{ Γ ⊢ A ⊆ Type@i }}) as [? [? _]] by mauto 2.
+  assert (exists a, ρ x = d{{{ ⇑! a (length Γ - x - 1) }}}) as [? Heq] by mauto 2.
  destruct Histyp;
    invert_rel_typ_body;
    destruct_conjs;
+    rewrite Heq in *;
    match_by_head1 per_univ_elem invert_per_univ_elem.
-  reflexivity.
+  rename x1 into a0.
+  rename x2 into x1.
+  assert (exists A, {{ #x1 : A ∈ Γ }} /\ {{ Γ ⊢ A ⊆ Type@i }}) as [? [? _]] by mauto 2.
+  assert (exists a, ρ x1 = d{{{ ⇑! a (length Γ - x1 - 1) }}}) as [a1] by mauto 2.
+  assert (x0 < length Γ) by mauto 2.
+  assert (x1 < length Γ) by mauto 2.
+  f_equal.
+  enough (length Γ - x0 - 1 = length Γ - x1 - 1) by lia.
+  replace (ρ x1) with d{{{ ⇑! a1 (length Γ - x1 - 1) }}} in * by intuition.
+  autoinjections.
+  match_by_head1 per_bot ltac:(fun H => destruct (H (length Γ)) as [? []]).
+  match_by_head read_ne ltac:(fun H => directed dependent destruction H).
+  lia.
Qed.
+#[export]
+Hint Resolve is_typ_constr_and_exp_eq_var_implies_eq_var : mcltt.

+Theorem is_typ_constr_and_exp_eq_typ_implies_eq_typ : forall Γ A i j,
+    is_typ_constr A ->
+    {{ Γ ⊢ A ≈ Type@i : Type@j }} ->
+    A = {{{ Type@i }}}.
+Proof.
+  intros * Histyp ?.
+  assert {{ Γ ⊨ A ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  destruct Histyp;
+    invert_rel_typ_body;
+    destruct_conjs;
+    match_by_head1 per_univ_elem invert_per_univ_elem.
+  - reflexivity.
+  - replace {{{ #x0 }}} with {{{ Type@i }}} by mauto 3 using is_typ_constr_and_exp_eq_var_implies_eq_var.
+    reflexivity.
+Qed.
#[export]
Hint Resolve is_typ_constr_and_exp_eq_typ_implies_eq_typ : mcltt.

-Theorem is_typ_constr_and_exp_eq_nat_implies_eq_nat : forall Γ A j,
-    is_typ_constr A ->
-    {{ Γ ⊢ A ≈ ℕ : Type@j }} ->
-    A = {{{ ℕ }}}.
+Theorem is_typ_constr_and_exp_eq_nat_implies_eq_nat : forall Γ A j,
+    is_typ_constr A ->
+    {{ Γ ⊢ A ≈ ℕ : Type@j }} ->
+    A = {{{ ℕ }}}.
Proof.
  intros * Histyp ?.
-  assert {{ Γ ⊨ A ≈ ℕ : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  assert {{ Γ ⊨ A ≈ ℕ : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
  destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
  destruct_conjs.
  functional_initial_env_rewrite_clear.
  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -117,7 +156,9 @@

Mcltt.Core.Completeness.Consequences.Types

    invert_rel_typ_body;
    destruct_conjs;
    match_by_head1 per_univ_elem invert_per_univ_elem.
-  reflexivity.
+  - reflexivity.
+  - replace {{{ #x0 }}} with {{{ ℕ }}} by mauto 3 using is_typ_constr_and_exp_eq_var_implies_eq_var.
+    reflexivity.
Qed.

diff --git a/Mcltt.Core.Semantic.Consequences.html b/Mcltt.Core.Semantic.Consequences.html index e514876..86a7f1e 100644 --- a/Mcltt.Core.Semantic.Consequences.html +++ b/Mcltt.Core.Semantic.Consequences.html @@ -35,11 +35,26 @@

Mcltt.Core.Semantic.Consequences

Import Domain_Notations.

-Lemma adjust_exp_eq_level : forall {Γ A A' i j},
-    {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ ⊢ A : Type@j }} ->
-    {{ Γ ⊢ A' : Type@j }} ->
-    {{ Γ ⊢ A ≈ A' : Type@j }}.
+Lemma idempotent_nbe_ty : forall {Γ i A B C},
+    {{ Γ ⊢ A : Type@i }} ->
+    nbe_ty Γ A B ->
+    nbe_ty Γ B C ->
+    B = C.
+Proof.
+  intros.
+  assert {{ Γ ⊢ A ≈ B : Type@i }} as [? []]%completeness_ty by mauto 2 using soundness_ty'.
+  functional_nbe_rewrite_clear.
+  reflexivity.
+Qed.
+#[export]
+Hint Resolve idempotent_nbe_ty : mcltt.
+ +
+Lemma adjust_exp_eq_level : forall {Γ A A' i j},
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ A : Type@j }} ->
+    {{ Γ ⊢ A' : Type@j }} ->
+    {{ Γ ⊢ A ≈ A' : Type@j }}.
Proof.
  intros * ?%completeness ?%soundness ?%soundness.
  destruct_conjs.
@@ -53,9 +68,9 @@

Mcltt.Core.Semantic.Consequences

Qed.

-Lemma exp_eq_pi_inversion : forall {Γ A B A' B' i},
-    {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }} /\ {{ Γ, A ⊢ B ≈ B' : Type@i }}.
+Lemma exp_eq_pi_inversion : forall {Γ A B A' B' i},
+    {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} /\ {{ Γ, A ⊢ B ≈ B' : Type@i }}.
Proof.
  intros * H.
  gen_presups.
@@ -72,15 +87,16 @@

Mcltt.Core.Semantic.Consequences

  functional_eval_rewrite_clear.
  functional_read_rewrite_clear.
  match_by_head (@eq nf) ltac:(fun H => directed inversion H; subst; clear H).
-  assert {{ Γ ⊢ A ≈ A' : Type@i }} by mauto.
-  assert {{ ⊢ Γ, A ≈ Γ, A' }} by mauto.
-  split; mauto.
+  assert {{ Γ ⊢ A ≈ A' : Type@i }} by mauto.
+  assert {{ ⊢ Γ, A ≈ Γ, A' }} by mauto.
+  split; [mauto 3 |].
+  etransitivity; mauto 4.
Qed.

-Lemma nf_of_pi : forall {Γ M A B},
-    {{ Γ ⊢ M : Π A B }} ->
-    exists W1 W2, nbe Γ M {{{ Π A B }}} n{{{ λ W1 W2 }}}.
+Lemma nf_of_pi : forall {Γ M A B},
+    {{ Γ ⊢ M : Π A B }} ->
+    exists W1 W2, nbe Γ M {{{ Π A B }}} n{{{ λ W1 W2 }}}.
Proof.
  intros * ?%soundness.
  destruct_conjs.
@@ -89,23 +105,143 @@

Mcltt.Core.Semantic.Consequences

  match_by_head1 read_nf ltac:(fun H => inversion_clear H).
  do 2 eexists; mauto.
Qed.
+#[export]
+Hint Resolve nf_of_pi : mcltt.
+ +
+Theorem canonical_form_of_pi : forall {M A B},
+    {{ ⋅ ⊢ M : Π A B }} ->
+    exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π A B }}} n{{{ λ W1 W2 }}}.
+Proof. mauto. Qed.
+#[export]
+Hint Resolve canonical_form_of_pi : mcltt.
+ +
+Inductive canonical_nat : nf -> Prop :=
+| canonical_nat_zero : canonical_nat n{{{ zero }}}
+| canonical_nat_succ : forall W, canonical_nat W -> canonical_nat n{{{ succ W }}}
+.
+#[export]
+Hint Constructors canonical_nat : mcltt.
+ +
+Theorem canonical_form_of_nat : forall {M},
+    {{ ⋅ ⊢ M : ℕ }} ->
+    exists W, nbe {{{ ⋅ }}} M {{{ ℕ }}} W /\ canonical_nat W.
+Proof with mautosolve 4.
+  intros * [? []]%soundness.
+  eexists; split; [eassumption |].
+  inversion_clear_by_head nbe.
+  invert_rel_typ_body.
+  match_by_head1 eval_exp ltac:(fun H => clear H).
+  gen M.
+  match_by_head1 read_nf ltac:(fun H => dependent induction H);
+    intros; mauto 3;
+    gen_presups.
+  - assert ({{ ⋅ ⊢ M : ℕ }} /\ {{ ⋅ ⊢ ℕ ⊆ ℕ }}) as [? _]...
+  - exfalso.
+    eapply no_closed_neutral...
+Qed.
+#[export]
+Hint Resolve canonical_form_of_nat : mcltt.

-Lemma idempotent_nbe_ty : forall {Γ i A B C},
-    {{ Γ ⊢ A : Type@i }} ->
-    nbe_ty Γ A B ->
-    nbe_ty Γ B C ->
-    B = C.
+Lemma subtyp_spec : forall {Γ A B},
+    {{ Γ ⊢ A ⊆ B }} ->
+    (exists k, {{ Γ ⊢ A ≈ B : Type@k }}) \/
+      (exists i j, (exists k, {{ Γ ⊢ A ≈ Type@i : Type@k }}) /\ (exists k, {{ Γ ⊢ Type@j ≈ B : Type@k }}) /\ i <= j) \/
+      (exists A1 A2 B1 B2, (exists k, {{ Γ ⊢ A ≈ Π A1 A2 : Type@k }}) /\ (exists k, {{ Γ ⊢ Π B1 B2 ≈ B : Type@k }}) /\ (exists k, {{ Γ ⊢ A1 ≈ B1 : Type@k }}) /\ {{ Γ, B1 ⊢ A2 ⊆ B2 }}).
Proof.
-  intros.
-  assert {{ Γ ⊢ A ≈ B : Type@i }} as [? []]%completeness_ty by mauto 2 using soundness_ty'.
-  functional_nbe_rewrite_clear.
-  reflexivity.
+  induction 1; mauto 3.
+  - destruct_all; firstorder (mauto 3);
+      try (right; right; do 4 eexists; repeat split; mautosolve 3).
+    + right; left.
+      match goal with
+      | _: {{ Γ ⊢ M' ≈ Type@?i : Type@_ }},
+          _: {{ Γ ⊢ Type@?j ≈ M' : Type@_ }} |- _ =>
+          assert {{ Γ ⊢ Type@j ≈ Type@i : Type@_ }} by mauto 3;
+          assert (j = i) as -> by mauto 3
+      end.
+      do 2 eexists; repeat split; mauto 3; lia.
+    + assert {{ Γ ⊢ Π ~_ ~_ ≈ Type@_ : Type@_ }} by mauto 3.
+      assert ({{{ Π ~_ ~_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
+    + right; left.
+      assert {{ Γ ⊢ Π ~_ ~_ ≈ Type@_ : Type@_ }} by mauto 3.
+      assert ({{{ Π ~_ ~_ }}} = {{{ Type@_ }}}) by mauto 3; congruence.
+    + right; right.
+      match goal with
+      | _: {{ Γ ⊢ M' ≈ Π ~?A1 ~?A2 : Type@_ }},
+          _: {{ Γ ⊢ Π ~?B1 ~?B2 ≈ M' : Type@_ }} |- _ =>
+          assert {{ Γ ⊢ Π A1 A2 ≈ Π B1 B2 : Type@_ }} by mauto 3;
+          assert ({{ Γ ⊢ A1 ≈ B1 : Type@_ }} /\ {{ Γ, A1 ⊢ A2 ≈ B2 : Type@_ }}) as [] by mauto 3 using exp_eq_pi_inversion
+      end.
+      do 4 eexists; repeat split; mauto 3.
+      * eexists; mauto 4.
+      * etransitivity; mauto 3.
+        etransitivity; eapply ctxeq_subtyp; mauto 3; eapply wf_ctx_eq_extend'; mauto 3.
+  - right; left.
+    do 2 eexists; repeat split; mauto 4; lia.
+  - right; right.
+    do 4 eexists; repeat split; mauto 4.
Qed.

#[export]
-Hint Resolve idempotent_nbe_ty : mcltt.
+Hint Resolve subtyp_spec : mcltt.
+ +
+Lemma consistency_ne_helper : forall {i T T'} {W : ne},
+    is_typ_constr T' ->
+    (forall j, T' <> {{{ Type@j }}}) ->
+    {{ ⋅, Type@i ⊢ T ⊆ T' }} ->
+    ~ {{ ⋅, Type@i ⊢ W : T }}.
+Proof.
+  intros * HT' HT'eq Heq HW. gen T'.
+  dependent induction HW; intros; mauto 3; try directed dependent destruction HT';
+    try (destruct W; simpl in *; congruence).
+  - destruct W; simpl in *; autoinjections.
+    eapply IHHW4; [| | | | mauto 4]; mauto 3; congruence.
+  - destruct W; simpl in *; autoinjections.
+    eapply IHHW3; [| | | | mauto 4]; mauto 3; congruence.
+  - destruct W; simpl in *; autoinjections.
+    do 2 match_by_head ctx_lookup ltac:(fun H => dependent destruction H).
+    assert {{ ⋅, Type@i ⊢ Type@i[Wk] ≈ Type@i : Type@(S i) }} by mauto 3.
+    eapply subtyp_spec in Heq as [| []]; destruct_conjs;
+      try (eapply HT'eq; mautosolve 4).
+    assert {{ ⋅, Type@i ⊢ Type@i ≈ Π ~_ ~_ : Type@_ }} by mauto 3.
+    assert ({{{ Π ~_ ~_ }}} = {{{ Type@i }}}) by mauto 3.
+    congruence.
+Qed.
+ +
+Theorem consistency : forall {i} M,
+    ~ {{ ⋅ ⊢ M : Π Type@i #0 }}.
+Proof.
+  intros * HW.
+  assert (exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π Type@i #0 }}} n{{{ λ W1 W2 }}}) as [? [? Hnbe]] by mauto 3.
+  assert (exists W, nbe {{{ ⋅ }}} M {{{ Π Type@i #0 }}} W /\ {{ ⋅ ⊢ M ≈ W : Π Type@i #0 }}) as [? []] by mauto 3 using soundness.
+  gen_presups.
+  functional_nbe_rewrite_clear.
+  dependent destruction Hnbe.
+  invert_rel_typ_body.
+  match_by_head read_nf ltac:(fun H => directed dependent destruction H).
+  match_by_head read_typ ltac:(fun H => directed dependent destruction H).
+  invert_rel_typ_body.
+  match_by_head read_nf ltac:(fun H => directed dependent destruction H).
+  simpl in *.
+  assert (exists B, {{ ⋅, Type@i ⊢ M0 : B }} /\ {{ ⋅ ⊢ Π Type@i B ⊆ Π Type@i #0 }}) as [? [? [| []]%subtyp_spec]] by mauto 3;
+    destruct_conjs;
+    try assert ({{{ Π ~_ ~_ }}} = {{{ Type@_ }}}) by mauto 3;
+    try congruence.
+  - assert (_ /\ {{ ⋅, Type@i ⊢ ~_ ≈ #0 : ~_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
+    eapply consistency_ne_helper; mauto 3.
+    congruence.
+  - assert (_ /\ {{ ~_ ⊢ x ≈ ~_ : ~_ }}) as [_ ?] by mauto 3 using exp_eq_pi_inversion.
+    assert (_ /\ {{ ~_ ⊢ ~_ ≈ #0 : ~_ }}) as [? ?] by mauto 3 using exp_eq_pi_inversion.
+    assert {{ ⋅, Type@i ⊢ x ⊆ #0 }} by (etransitivity; [| eapply ctxeq_subtyp]; mauto 4).
+    eapply consistency_ne_helper; mauto 3.
+    congruence.
+Qed.
+ +
+In the following spec, we do not care (for now) + whether a is the evaluation result of A or not. + If we want to specify that as well, we need a generalized + version of drop_env that can drop x elements. +
+
+Lemma initial_env_spec : forall x Γ ρ A,
+    initial_env Γ ρ ->
+    {{ #x : A ∈ Γ }} ->
+    exists a, ρ x = d{{{ ⇑! a (length Γ - x - 1) }}}.
+Proof.
+  induction x; intros * Hinit Hlookup;
+    dependent destruction Hlookup; dependent destruction Hinit; simpl; mauto 3.
+  eexists; repeat f_equal; lia.
+Qed.
+ +
+#[export]
+Hint Resolve initial_env_spec : mcltt.
+
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
@@ -78,20 +103,20 @@

Mcltt.Core.Semantic.NbE

Inductive nbe : ctx -> exp -> typ -> nf -> Prop :=
| nbe_run :
  `( initial_env Γ ρ ->
-     {{ ⟦ A ⟧ ρ ↘ a }} ->
-     {{ ⟦ M ⟧ ρ ↘ m }} ->
-     {{ Rnf ⇓ a m in (length Γ) ↘ w }} ->
-     nbe Γ M A w ).
+     {{ ⟦ A ⟧ ρ ↘ a }} ->
+     {{ ⟦ M ⟧ ρ ↘ m }} ->
+     {{ Rnf ⇓ a m in (length Γ) ↘ w }} ->
+     nbe Γ M A w ).

#[export]
Hint Constructors nbe : mcltt.

-Lemma functional_nbe : forall Γ M A w w',
-    nbe Γ M A w ->
-    nbe Γ M A w' ->
-    w = w'.
+Lemma functional_nbe : forall Γ M A w w',
+    nbe Γ M A w ->
+    nbe Γ M A w' ->
+    w = w'.
Proof.
  intros.
  inversion_clear H; inversion_clear H0;
@@ -106,9 +131,9 @@

Mcltt.Core.Semantic.NbE

Hint Resolve functional_nbe : mcltt.

-Lemma nbe_cumu : forall {Γ A i W},
-    nbe Γ A {{{ Type@i }}} W ->
-    nbe Γ A {{{ Type@(S i) }}} W.
+Lemma nbe_cumu : forall {Γ A i W},
+    nbe Γ A {{{ Type@i }}} W ->
+    nbe Γ A {{{ Type@(S i) }}} W.
Proof.
  inversion_clear 1.
  simplify_evals.
@@ -117,18 +142,18 @@

Mcltt.Core.Semantic.NbE

Qed.

-Lemma lift_nbe_ge : forall {Γ A i j W},
-    i <= j ->
-    nbe Γ A {{{ Type@i }}} W ->
-    nbe Γ A {{{ Type@j }}} W.
+Lemma lift_nbe_ge : forall {Γ A i j W},
+    i <= j ->
+    nbe Γ A {{{ Type@i }}} W ->
+    nbe Γ A {{{ Type@j }}} W.
Proof.
  induction 1; mauto using nbe_cumu.
Qed.

-Lemma lift_nbe_max_left : forall {Γ A i i' W},
-    nbe Γ A {{{ Type@i }}} W ->
-    nbe Γ A {{{ Type@(max i i') }}} W.
+Lemma lift_nbe_max_left : forall {Γ A i i' W},
+    nbe Γ A {{{ Type@i }}} W ->
+    nbe Γ A {{{ Type@(max i i') }}} W.
Proof.
  intros.
  assert (i <= max i i') by lia.
@@ -136,9 +161,9 @@

Mcltt.Core.Semantic.NbE

Qed.

-Lemma lift_nbe_max_right : forall {Γ A i i' W},
-    nbe Γ A {{{ Type@i' }}} W ->
-    nbe Γ A {{{ Type@(max i i') }}} W.
+Lemma lift_nbe_max_right : forall {Γ A i i' W},
+    nbe Γ A {{{ Type@i' }}} W ->
+    nbe Γ A {{{ Type@(max i i') }}} W.
Proof.
  intros.
  assert (i' <= max i i') by lia.
@@ -150,10 +175,10 @@

Mcltt.Core.Semantic.NbE

Hint Resolve lift_nbe_max_left lift_nbe_max_right : mcltt.

-Lemma functional_nbe_of_typ : forall Γ A i j W W',
-    nbe Γ A {{{ Type@i }}} W ->
-    nbe Γ A {{{ Type@j }}} W' ->
-    W = W'.
+Lemma functional_nbe_of_typ : forall Γ A i j W W',
+    nbe Γ A {{{ Type@i }}} W ->
+    nbe Γ A {{{ Type@j }}} W' ->
+    W = W'.
Proof.
  mauto.
Qed.
@@ -166,19 +191,19 @@

Mcltt.Core.Semantic.NbE

Inductive nbe_ty : ctx -> typ -> nf -> Prop :=
| nbe_ty_run :
  `( initial_env Γ ρ ->
-     {{ ⟦ M ⟧ ρ ↘ m }} ->
-     {{ Rtyp m in (length Γ) ↘ W }} ->
-     nbe_ty Γ M W ).
+     {{ ⟦ M ⟧ ρ ↘ m }} ->
+     {{ Rtyp m in (length Γ) ↘ W }} ->
+     nbe_ty Γ M W ).

#[export]
Hint Constructors nbe_ty : mcltt.

-Lemma functional_nbe_ty : forall Γ M w w',
-    nbe_ty Γ M w ->
-    nbe_ty Γ M w' ->
-    w = w'.
+Lemma functional_nbe_ty : forall Γ M w w',
+    nbe_ty Γ M w ->
+    nbe_ty Γ M w' ->
+    w = w'.
Proof.
  intros.
  inversion_clear H; inversion_clear H0;
@@ -189,9 +214,9 @@

Mcltt.Core.Semantic.NbE

Qed.

-Lemma nbe_type_to_nbe_ty : forall Γ M i w,
-    nbe Γ M {{{ Type@i }}} w ->
-    nbe_ty Γ M w.
+Lemma nbe_type_to_nbe_ty : forall Γ M i w,
+    nbe Γ M {{{ Type@i }}} w ->
+    nbe_ty Γ M w.
Proof.
  intros. progressive_inversion.
  mauto.
diff --git a/Mcltt.Core.Syntactic.System.Lemmas.html b/Mcltt.Core.Syntactic.System.Lemmas.html index 5864742..c60d844 100644 --- a/Mcltt.Core.Syntactic.System.Lemmas.html +++ b/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.
@@ -194,10 +204,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.
@@ -209,10 +219,10 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve exp_sub_typ : mcltt.

-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.
@@ -232,21 +242,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.

@@ -262,10 +272,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; intros; mauto.
Qed.
@@ -275,28 +285,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; mauto.
Qed.
@@ -306,18 +316,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...
@@ -333,15 +343,15 @@

Mcltt.Core.Syntactic.System.Lemmas


-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 * HΓ.
  induction 1; inversion_clear HΓ;
-    [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.

@@ -349,22 +359,22 @@

Mcltt.Core.Syntactic.System.Lemmas

Hint Resolve presup_ctx_lookup_typ : mcltt.

-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 : Γ, ℕ }} by mauto 3.
+  induction 1; assert {{ ⊢ Γ }} by mauto 3; destruct_conjs; mauto 3.
+  - enough {{ Γ ⊢s Id,,M : Γ, ℕ }} by mauto 3.
    do 3 (econstructor; mauto 3).
  - eexists; mauto 4 using lift_exp_max_left, lift_exp_max_right.
-  - enough {{ Γ ⊢s Id,,N : Γ, A }} by mauto 3.
+  - enough {{ Γ ⊢s Id,,N : Γ, A }} by mauto 3.
    do 3 (econstructor; mauto 3).
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.
@@ -379,9 +389,9 @@

Mcltt.Core.Syntactic.System.Lemmas


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

@@ -389,17 +399,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.

@@ -407,10 +417,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.

@@ -418,17 +428,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.

@@ -436,10 +446,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.

@@ -447,7 +457,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.
@@ -463,9 +473,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.

@@ -473,14 +483,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.

@@ -488,9 +498,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.

@@ -507,32 +517,32 @@

Mcltt.Core.Syntactic.System.Lemmas


-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...
@@ -543,10 +553,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.

@@ -556,10 +566,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';
@@ -568,9 +578,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.
@@ -578,13 +588,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.
@@ -593,10 +603,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).
@@ -607,10 +617,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.
@@ -618,16 +628,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.
@@ -638,16 +648,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.
@@ -656,10 +666,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...
@@ -670,11 +680,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.
@@ -682,25 +692,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.
@@ -709,15 +719,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 (Wk∘Id),,#0[Id] ≈ Id : Γ, A }} by mauto.
-  assert {{ Γ, A ⊢s Wk ≈ Wk∘Id : Γ }} by mauto.
-  enough {{ Γ, A ⊢ #0 ≈ #0[Id] : A[Wk] }}...
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢s (Wk∘Id),,#0[Id] ≈ Id : Γ, A }} by mauto.
+  assert {{ Γ, A ⊢s Wk ≈ Wk∘Id : Γ }} by mauto.
+  enough {{ Γ, A ⊢ #0 ≈ #0[Id] : A[Wk] }}...
Qed.

@@ -727,19 +737,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.

@@ -756,32 +766,32 @@

Mcltt.Core.Syntactic.System.Lemmas


-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...
@@ -792,10 +802,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.

@@ -803,11 +813,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.

@@ -815,9 +825,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.
@@ -825,13 +835,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.
@@ -840,10 +850,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).
@@ -854,10 +864,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.
@@ -865,16 +875,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.

@@ -882,15 +892,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.

@@ -898,10 +908,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...
@@ -912,11 +922,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.
@@ -924,24 +934,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.
@@ -950,19 +960,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.

@@ -979,22 +989,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.
@@ -1003,13 +1013,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ΓΔ'];
@@ -1021,10 +1031,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...
@@ -1035,10 +1045,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...
@@ -1049,10 +1059,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...
@@ -1065,43 +1075,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.

@@ -1109,25 +1119,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.
@@ -1136,48 +1146,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.

@@ -1185,17 +1195,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.
@@ -1204,26 +1214,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.
@@ -1234,15 +1244,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.
@@ -1251,12 +1261,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.

@@ -1264,22 +1274,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 Wk∘q (q σ) ≈ q σ ∘ Wk : Δ, ℕ }} by mauto.
-  assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (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 Wk∘q (q σ) ≈ q σ ∘ Wk : Δ, ℕ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (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.

@@ -1287,52 +1297,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 := {{{ (Wk∘Wk),,succ #1 }}}).
-  assert {{ ⊢ Γ' }} by mauto 2.
-  assert {{ Γ' ⊢s Wk∘Wk : Γ }} 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 Wk∘WkWksucc : Γ }} by mauto 4.
-  assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto 4.
-  assert {{ Γ ⊢s σ ≈ σ : Δ }} by mauto.
-  assert {{ Γ' ⊢s σ∘(Wk∘WkWksucc) ≈ σ∘(Wk∘Wk) : Δ }} by mauto 3.
-  assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ≈ σ∘(Wk∘Wk) : Δ }} by mauto 3.
-  assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (σ∘Wk)∘Wk : Δ }} by mauto 4.
-  assert {{ Γ' ⊢s (σ∘Wk)∘Wk ≈ Wk∘(Wk∘q (q σ)) : Δ }} by mauto.
-  assert {{ Δ, ℕ ⊢s Wk : Δ }} by mauto 4.
-  assert {{ Δ, ℕ, A ⊢s Wk : Δ, ℕ }} by mauto 4.
-  assert {{ Δ, ℕ, A ⊢s Wk∘Wk : Δ }} by mauto 4.
-  assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, A }} by mauto.
-  assert {{ Γ' ⊢s Wk∘(Wk∘q (q σ)) ≈ (Wk∘Wk)∘q (q σ) : Δ }} by mauto 3.
-  assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (Wk∘Wk)∘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] ≈ ((Wk∘Wk)∘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 ((Wk∘Wk)∘q (q σ)),,(succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
+  assert {{ ⊢ Γ' }} by mauto 2.
+  assert {{ Γ' ⊢s Wk∘Wk : Γ }} 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 Wk∘WkWksucc : Γ }} by mauto 4.
+  assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto 4.
+  assert {{ Γ ⊢s σ ≈ σ : Δ }} by mauto.
+  assert {{ Γ' ⊢s σ∘(Wk∘WkWksucc) ≈ σ∘(Wk∘Wk) : Δ }} by mauto 3.
+  assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ≈ σ∘(Wk∘Wk) : Δ }} by mauto 3.
+  assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (σ∘Wk)∘Wk : Δ }} by mauto 4.
+  assert {{ Γ' ⊢s (σ∘Wk)∘Wk ≈ Wk∘(Wk∘q (q σ)) : Δ }} by mauto.
+  assert {{ Δ, ℕ ⊢s Wk : Δ }} by mauto 4.
+  assert {{ Δ, ℕ, A ⊢s Wk : Δ, ℕ }} by mauto 4.
+  assert {{ Δ, ℕ, A ⊢s Wk∘Wk : Δ }} by mauto 4.
+  assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, A }} by mauto.
+  assert {{ Γ' ⊢s Wk∘(Wk∘q (q σ)) ≈ (Wk∘Wk)∘q (q σ) : Δ }} by mauto 3.
+  assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (Wk∘Wk)∘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] ≈ ((Wk∘Wk)∘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 ((Wk∘Wk)∘q (q σ)),,(succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
Qed.

@@ -1349,9 +1359,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.

@@ -1359,10 +1369,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.
@@ -1372,18 +1382,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.
@@ -1392,10 +1402,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.
@@ -1405,13 +1415,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.
@@ -1422,6 +1432,20 @@

Mcltt.Core.Syntactic.System.Lemmas


#[export]
Hint Resolve ctx_sub_ctx_lookup : mcltt.
+ +
+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.