one more rule

theories/Core/Completeness/SubstitutionCases.v

@@ -306,3 +306,7 @@ Proof.
   econstructor; eauto.
   eapply per_ctx_env_subtyping; eauto.
 Qed.
+
+
+#[export]
+  Hint Resolve wf_sub_eq_subtyp' : mcltt.

theories/Core/Completeness/SubtypingCases.v

@@ -0,0 +1,56 @@
+From Coq Require Import Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness.LogicalRelation Evaluation.
+Import Domain_Notations.
+
+
+Lemma wf_subtyp_refl' : forall Γ M M' i,
+    {{ Γ ⊨ M ≈ M' : Type@i }} ->
+    {{ Γ ⊨ M ⊆ M' }}.
+Proof.
+  intros * [R [HR [i H]]].
+  do 3 try eexists; eauto.
+  intros.
+  saturate_refl.
+  destruct (H _ _ equiv_p_p') as [elem_relpp' [[] []]].
+  destruct (H _ _ H0) as [elem_relpp [[] []]].
+  destruct (H _ _ H1) as [elem_relp'p' [[] []]].
+  repeat match goal with
+         | H : eval_exp _ _ _ |- _ => progressive_invert H
+         end.
+  simplify_evals.
+  on_all_hyp: fun H => directed invert_per_univ_elem H.
+  apply_equiv_left.
+  destruct_all.
+  handle_per_univ_elem_irrel.
+  do 2 eexists. repeat split.
+  - econstructor; eauto.
+    etransitivity; [eassumption |].
+    symmetry. eassumption.
+  - econstructor; eauto.
+    etransitivity; [symmetry; eassumption |].
+    eassumption.
+  - econstructor; eauto.
+    eauto using per_subtyp_refl1.
+Qed.
+
+(* | wf_subtyp_trans : *)
+(*   `( {{ Γ ⊢ M ⊆ M' }} -> *)
+(*      {{ Γ ⊢ M' ⊆ M'' }} -> *)
+(*      {{ Γ ⊢ M ⊆ M'' }} ) *)
+(* | wf_subtyp_univ : *)
+(*   `( {{ ⊢ Γ }} -> *)
+(*      i < j -> *)
+(*      {{ Γ ⊢ Type@i ⊆ Type@j }} ) *)
+(* | wf_subtyp_pi : *)
+(*   `( {{ Γ ⊢ A : Type@i }} -> *)
+(*      {{ Γ ⊢ A' : Type@i }} -> *)
+(*      {{ Γ ⊢ A ≈ A' : Type@i }} -> *)
+(*      {{ Γ , A ⊢ B : Type@i }} -> *)
+(*      {{ Γ , A' ⊢ B' : Type@i }} -> *)
+(*      {{ Γ , A' ⊢ B ⊆ B' }} -> *)
+(*      {{ Γ ⊢ Π A B ⊆ Π A' B' }} ) *)
+
+
+#[export]
+ Hint Resolve wf_subtyp_refl' : mcltt.

theories/_CoqProject

@@ -21,6 +21,7 @@
 ./Core/Completeness/TermStructureCases.v
 ./Core/Completeness/UniverseCases.v
 ./Core/Completeness/VariableCases.v
+./Core/Completeness/SubtypingCases.v
 ./Core/Completeness.v
 ./Core/Semantic/Consequences.v
 ./Core/Semantic/Domain.v