Working on subtyping

theories/Core/Syntactic/CoreInversions.v

@@ -1,5 +1,5 @@
 From Coq Require Import Setoid.
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import Base LibTactics CtxSub.
 From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
@@ -79,7 +79,7 @@ Lemma wf_vlookup_inversion : forall {Γ x A},
 Proof with mautosolve 4.
   intros * H.
   dependent induction H;
-    [assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by mauto 4 | |];
+    [assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by mauto 4 |];
     try (specialize (IHwf_exp _ eq_refl));
     destruct_conjs;
     eexists; split...
@@ -107,7 +107,7 @@ Hint Resolve wf_exp_sub_inversion : mcltt.
 
 Lemma wf_sub_id_inversion : forall Γ Δ,
     {{ Γ ⊢s Id : Δ }} ->
-    {{ ⊢ Γ ≈ Δ }}.
+    {{ ⊢ Γ ⊆ Δ }}.
 Proof.
   intros * H.
   dependent induction H; mautosolve.
@@ -118,15 +118,13 @@ Hint Resolve wf_sub_id_inversion : mcltt.
 
 Lemma wf_sub_weaken_inversion : forall {Γ Δ},
     {{ Γ ⊢s Wk : Δ }} ->
-    exists A, {{ ⊢ Γ ≈ Δ, A }}.
-Proof with mautosolve 4.
+    exists Γ' A, {{ ⊢ Γ ≈ Γ', A }} /\ {{ ⊢ Γ' ⊆ Δ }}.
+Proof.
   intros * H.
-  dependent induction H; mauto.
-  specialize (IHwf_sub eq_refl).
-  destruct_conjs.
-  gen_presups.
-  eexists.
-  etransitivity...
+  dependent induction H;
+    firstorder;
+    progressive_inversion;
+    repeat eexists; mauto.
 Qed.
 
 #[export]
@@ -149,13 +147,13 @@ Hint Resolve wf_sub_compose_inversion : mcltt.
 
 Lemma wf_sub_extend_inversion : forall {Γ σ M Δ},
     {{ Γ ⊢s σ,,M : Δ }} ->
-    exists Δ' A', {{ ⊢ Δ ≈ Δ', A' }} /\ {{ Γ ⊢s σ : Δ' }} /\ {{ Γ ⊢ M : A'[σ] }}.
+    exists Δ' A', {{ ⊢ Δ', A' ⊆ Δ }} /\ {{ Γ ⊢s σ : Δ' }} /\ {{ Γ ⊢ M : A'[σ] }}.
 Proof with mautosolve 4.
   intros * H.
   dependent induction H;
     try specialize (IHwf_sub _ _ eq_refl);
     destruct_conjs;
-    do 2 eexists; split...
+    repeat eexists...
 Qed.
 
 #[export]

theories/Core/Syntactic/CtxEq.v

@@ -1,4 +1,4 @@
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import Base LibTactics CtxSub.
 From Mcltt Require Export System.
 Import Syntax_Notations.
 
@@ -18,75 +18,34 @@ Qed.
 #[export]
 Hint Resolve ctx_eq_sym : mcltt.
 
-Module ctxeq_judg.
-  #[local]
-  Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
-  match type of H with
-  | {{ ~?Γ ⊢ ~?M : ~?A }} => pose proof ctxeq_exp_helper _ _ _ H
-  | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
-  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
-  | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
-  end.
-
-  #[local]
-  Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
-  with
-  ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
-  with
-  ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
-  with
-  ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
-  Proof with mautosolve.
-    all: inversion_clear 1;
-      (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
-      clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
-      intros * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto 4;
-      try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
-    (* ctxeq_exp_helper & ctxeq_exp_eq_helper recursion cases *)
-    1,6-8: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mautosolve);
-      assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
-    (* ctxeq_exp_helper & ctxeq_exp_eq_helper function cases *)
-    1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto;
-      try econstructor...
-    (* ctxeq_exp_helper & ctxeq_exp_eq_helper variable cases *)
-    1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs; mautosolve 4.
-    (* ctxeq_sub_helper & ctxeq_sub_eq_helper weakening cases *)
-    2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
-
-    (* ctxeq_exp_eq_helper variable case *)
-    inversion_clear HΓΔ as [|? Δ0 ? ? C'].
-    assert (exists D i', {{ #x : D ∈ Δ0 }} /\ {{ Γ0 ⊢ B ≈ D : Type@i' }} /\ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 ?]] by mauto.
-    destruct_conjs.
-    assert {{ ⊢ Δ0, C' }} by mauto.
-    assert {{ Δ0 ⊢ D ≈ B : Type@i0 }} by mauto.
-    assert {{ Δ0, C' ⊢ D[Wk] ≈ B[Wk] : Type@i0 }}...
-  Qed.
-
-  Corollary ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
-  Proof.
-    eauto using ctxeq_exp_helper.
-  Qed.
-
-  Corollary ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
-  Proof.
-    eauto using ctxeq_exp_eq_helper.
-  Qed.
-
-  Corollary ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
-  Proof.
-    eauto using ctxeq_sub_helper.
-  Qed.
-
-  Corollary ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
-  Proof.
-    eauto using ctxeq_sub_eq_helper.
-  Qed.
-
-  #[export]
-  Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq : mcltt.
-End ctxeq_judg.
-
-Export ctxeq_judg.
+Lemma ctx_eq_subtyping : forall Γ Δ,
+    {{ ⊢ Γ ≈ Δ }} ->
+    {{ ⊢ Γ ⊆ Δ }}.
+Proof.
+  induction 1; mauto 4.
+Qed.
+
+#[export]
+Hint Resolve ctx_eq_subtyping : mcltt.
+
+Lemma ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
+Proof. mauto. Qed.
+
+Lemma ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
+Proof. mauto. Qed.
+
+Lemma ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
+Proof. mauto. Qed.
+
+Lemma ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+Proof. mauto. Qed.
+
+Lemma ctxeq_subtyping : forall {Γ Δ A B}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ A ⊆ B }} -> {{ Δ ⊢ A ⊆ B }}.
+Proof. mauto. Qed.
+
+#[export]
+  Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq ctxeq_subtyping : mcltt.
+
 
 Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
 Proof with mautosolve.

theories/Core/Syntactic/CtxSub.v

@@ -0,0 +1,107 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export System.
+Import Syntax_Notations.
+
+Lemma ctx_sub_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ⊆ Γ }}.
+Proof with mautosolve.
+  induction 1...
+Qed.
+
+#[export]
+Hint Resolve ctx_sub_refl : mcltt.
+
+Module ctxsub_judg.
+  #[local]
+  Ltac gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyping_helper H :=
+  match type of H with
+  | {{ ~?Γ ⊢ ~?M : ~?A }} => pose proof ctxsub_exp_helper _ _ _ H
+  | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxsub_exp_eq_helper _ _ _ _ H
+  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxsub_sub_helper _ _ _ H
+  | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxsub_sub_eq_helper _ _ _ _ H
+  | {{ ~?Γ ⊢ ~?M ⊆ ~?M' }} => pose proof ctxsub_subtyping_helper _ _ _ H
+  end.
+
+  #[local]
+  Lemma ctxsub_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢ M : A }}
+  with
+  ctxsub_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢ M ≈ M' : A }}
+  with
+  ctxsub_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢s σ : Γ' }}
+  with
+  ctxsub_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}
+  with
+  ctxsub_subtyping_helper : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢ M ⊆ M' }}.
+  Proof with mautosolve.
+    all: inversion_clear 1;
+      (on_all_hyp: gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyping_helper);
+      clear ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyping_helper;
+      intros * HΓΔ; destruct (presup_ctx_sub HΓΔ); mauto 4;
+      try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
+    (* ctxsub_exp_helper & ctxsub_exp_eq_helper recursion cases *)
+    1,6-8: assert {{ ⊢ Δ, ℕ ⊆ Γ, ℕ }} by (econstructor; mautosolve);
+    assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
+    (* ctxsub_exp_helper & ctxsub_exp_eq_helper function cases *)
+    1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Δ, B ⊆ Γ, B }} by mauto;
+      try econstructor...
+    (* ctxsub_exp_helper & ctxsub_exp_eq_helper variable cases *)
+    1-2: assert (exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢  B ⊆ A }}); destruct_conjs; mautosolve 4.
+    (* ctxsub_sub_helper & ctxsub_sub_eq_helper weakening cases *)
+    2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
+
+    - (* ctxsub_exp_eq_helper variable case *)
+      inversion_clear HΓΔ as [|Δ0 ? C'].
+      assert (exists D, {{ #x : D ∈ Δ0 }} /\ {{ Δ0 ⊢ D ⊆ B }}) as [D [i0 ?]] by mauto.
+      destruct_conjs.
+      assert {{ ⊢ Δ0, C' }} by mauto.
+      assert {{ Δ0, C' ⊢ D[Wk] ⊆ B[Wk] }}...
+    - eapply wf_subtyp_pi with (i := i); firstorder mauto 4.
+  Qed.
+
+  Corollary ctxsub_exp : forall {Γ Δ M A}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
+  Proof.
+    eauto using ctxsub_exp_helper.
+  Qed.
+
+  Corollary ctxsub_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
+  Proof.
+    eauto using ctxsub_exp_eq_helper.
+  Qed.
+
+  Corollary ctxsub_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
+  Proof.
+    eauto using ctxsub_sub_helper.
+  Qed.
+
+  Corollary ctxsub_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+  Proof.
+    eauto using ctxsub_sub_eq_helper.
+  Qed.
+
+  Corollary ctxsub_subtyping : forall {Γ Δ A B}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢ A ⊆ B }} -> {{ Δ ⊢ A ⊆ B }}.
+  Proof.
+    eauto using ctxsub_subtyping_helper.
+  Qed.
+
+  #[export]
+  Hint Resolve ctxsub_exp ctxsub_exp_eq ctxsub_sub ctxsub_sub_eq ctxsub_subtyping : mcltt.
+End ctxsub_judg.
+
+Export ctxsub_judg.
+
+Lemma wf_ctx_sub_trans : forall Γ0 Γ1,
+    {{ ⊢ Γ0 ⊆ Γ1 }} ->
+    forall  Γ2,
+    {{ ⊢ Γ1 ⊆ Γ2 }} ->
+    {{ ⊢ Γ0 ⊆ Γ2 }}.
+Proof.
+  induction 1; intros; progressive_inversion; [constructor |].
+  eapply wf_ctx_sub_extend with (i := max i i0);
+    mauto 3 using lift_exp_max_left, lift_exp_max_right.
+Qed.
+
+#[export]
+ Hint Resolve wf_ctx_sub_trans : mcltt.
+
+#[export]
+  Instance wf_ctx_sub_trans_ins : Transitive wf_ctx_sub.
+Proof. eauto using wf_ctx_sub_trans. Qed.

theories/Core/Syntactic/Presup.v

@@ -9,14 +9,18 @@ Ltac gen_presup_ctx H :=
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_ctx_eq H as [HΓ HΔ]
+  | {{ ⊢ ~?Γ ⊆ ~?Δ }} =>
+      let HΓ := fresh "HΓ" in
+      let HΔ := fresh "HΔ" in
+      pose proof presup_ctx_sub H as [HΓ HΔ]
   | {{ ~?Γ ⊢s ~?σ : ~?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sub_ctx H as [HΓ HΔ]
   end.
 
 #[local]
-Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
+Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyping H :=
   match type of H with
   | {{ ~?Γ ⊢ ~?M : ~?A }} =>
       let HΓ := fresh "HΓ" in
@@ -36,16 +40,23 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
       let Hτ := fresh "Hτ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sub_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]
+  | {{ ~?Γ ⊢ ~?M ⊆ ~?N }} =>
+      let HΓ := fresh "HΓ" in
+      let i := fresh "i" in
+      let HM := fresh "HM" in
+      let HN := fresh "HN" in
+      pose proof presup_subtyping _ _ _ H as [HΓ [i [HM HN]]]
   | _ => gen_presup_ctx H
   end.
 
 Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
 with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
-with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}.
+with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}
+with presup_subtyping : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ M : Type@i }} /\ {{ Γ ⊢ M' : Type@i }}.
 Proof with mautosolve 4.
   2: set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
-  all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq);
-      clear presup_exp presup_exp_eq presup_sub_eq;
+  all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyping);
+    clear presup_exp presup_exp_eq presup_sub_eq presup_subtyping;
     repeat split; mauto 4;
     try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B');
     try (rename N into L); try (rename N' into L');
@@ -252,23 +263,16 @@ Proof with mautosolve 4.
   - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
     assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto.
     enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }}...
+
+    (* presup_subtyping cases *)
+  - exists (max i i0); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
+  - exists (max (S i) (S j)); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
+  - mauto.
 Qed.
 
 #[export]
-Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
+Hint Resolve presup_exp presup_exp_eq presup_sub_eq presup_subtyping : mcltt.
 
-Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq H.
+Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq @presup_subtyping H.
 
 Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx; clear_dups.
-
-Corollary typ_subsumption_presup : forall {Γ A A'},
-    {{ Γ ⊢ A ⊆ A' }} ->
-    {{ ⊢ Γ }} /\ (exists i, {{ Γ ⊢ A : Type@i }}) /\ (exists i', {{ Γ ⊢ A' : Type@i' }}).
-Proof.
-  intros * H.
-  dependent induction H; gen_presups; destruct_conjs; split; mauto 4.
-  split; eexists; mauto 4.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_presup : mcltt.