keep crushing it

theories/Core/Completeness/ContextCases.v

@@ -72,6 +72,6 @@ Proof.
   destruct H3 as [? [? []]].
   on_all_hyp: fun H => (eapply rel_ctx_extend' in H; destruct H).
   econstructor; mauto; intros.
-  deepexec H3 ltac:(fun H => destruct H as []).
+  deepexec H3 ltac:(fun H => destruct H as [? [? [? [? []]]]]).
   simplify_evals. eassumption.
 Qed.

theories/Core/Completeness/LogicalRelation/Definitions.v

@@ -48,7 +48,7 @@ Hint Unfold valid_sub_under_ctx : mcltt.
 Definition sub_typ_under_ctx Γ M M' :=
   exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
   forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
-    rel_exp M p M' p' (per_subtyp i).
+    exists R R', rel_typ i M p M p' R /\ rel_typ i M' p M' p' R' /\ rel_exp M p M' p' (per_subtyp i).
 
 Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
 Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).

theories/Core/Completeness/TermStructureCases.v

@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases.
+From Mcltt.Core Require Import Evaluation Completeness.LogicalRelation Completeness.UniverseCases.
 Import Domain_Notations.
 
 Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
@@ -187,3 +187,23 @@ Proof.
     (on_all_hyp: destruct_rel_by_assumption env_relΓ).
     eapply rel_typ_implies_rel_exp; eauto.
 Qed.
+
+
+Lemma wf_exp_eq_subtyp' : forall Γ M M' A A',
+    {{ Γ ⊨ M ≈ M' : A }} ->
+    {{ Γ ⊨ A ⊆ A' }} ->
+    {{ Γ ⊨ M ≈ M' : A' }}.
+Proof.
+  intros * [R [HR [i ?]]] [R' [HR' [j ?]]].
+  exists R. exists HR.
+  handle_per_ctx_env_irrel.
+  exists (max i j).
+  intros.
+  deepexec H ltac:(fun H => destruct H as [elem_rel [[] []]]).
+  apply_equiv_left.
+  deepexec H0 ltac:(fun H => destruct H as [R1 [R1' [[] [[] []]]]]).
+  simplify_evals.
+  exists R1'.
+  split.
+  - econstructor; eauto using per_univ_elem_cumu_max_right.
+  - econstructor; eauto.

theories/Core/Semantic/PER/Lemmas.v

@@ -653,6 +653,32 @@ Proof.
     deepexec H1 ltac:(fun H => apply H).
 Qed.
 
+Lemma per_elem_subtyping_gen : forall A B i A' B' R R' a b,
+    {{ Sub A <: B at i }} ->
+    {{ DF A ≈ A' ∈ per_univ_elem i ↘ R }} ->
+    {{ DF B ≈ B' ∈ per_univ_elem i ↘ R' }} ->
+    R a b ->
+    R' a b.
+Proof.
+  intros.
+  eapply per_elem_subtyping; try eassumption.
+  all:etransitivity; [| symmetry]; eassumption.
+Qed.
+
+(* Lemma per_subtyp_transp : forall A B i, *)
+(*     {{ Sub A <: B at i }} -> *)
+(*     forall A' B' R R', *)
+(*     {{ DF A ≈ A' ∈ per_univ_elem i ↘ R }} -> *)
+(*     {{ DF B ≈ B' ∈ per_univ_elem i ↘ R' }} -> *)
+(*     {{ Sub A' <: B' at i }}. *)
+(* Proof. *)
+(*   induction 1; intros; *)
+(*     (on_all_hyp: fun H => directed invert_per_univ_elem H); *)
+(*     apply_equiv_left; *)
+(*     mauto. *)
+(*   handle_per_univ_elem_irrel. *)
+(*   econstructor; eauto. *)
+
 Lemma per_subtyp_refl1 : forall a b i R,
     {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
     {{ Sub a <: b at i }}.