Update subtyping cases

theories/Core/Soundness/SubtypingCases.v

@@ -8,15 +8,14 @@ From Mcltt.Core.Syntactic Require Import Corollaries.
 Import Domain_Notations.
 
 Lemma glu_rel_exp_subtyp : forall {Γ M A A' i},
-    {{ Γ ⊩ A : Type@i }} ->
     {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊢ A ⊆ A' }} ->
     {{ Γ ⊩ M : A' }}.
 Proof.
-  intros * HA HA' [Sb [? [i]]] [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
+  intros * HA' [Sb [? [i]]] [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
   destruct_conjs.
-  eapply destruct_glu_rel_exp in HA, HA'; try eassumption.
+  eapply destruct_glu_rel_exp in HA'; try eassumption.
   destruct_conjs.
   rename i0 into k.
   econstructor; split; [eassumption |].
@@ -32,26 +31,35 @@ Proof.
   simplify_evals.
   match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
   handle_functional_glu_univ_elem.
-  simpl in *.
+  rename m into a'.
+  rename a0 into a.
+  rename m0 into m.
+  rename P0 into P.
+  rename El0 into El.
   assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by (eapply glu_ctx_env_per_env; mauto).
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   destruct_by_head rel_exp.
   handle_per_univ_elem_irrel.
-  assert (exists P El, glu_univ_elem (max i (max j k)) P El m0) as [? []].
+  unfold univ_glu_exp_pred' in *.
+  destruct_conjs.
+  assert (exists P El, glu_univ_elem (max i (max j k)) P El a') as [? []].
   {
-    assert (exists P El, glu_univ_elem (max j k) P El m0) as [? []];
+    assert (exists P El, glu_univ_elem (max j k) P El a') as [? []];
       mauto using glu_univ_elem_cumu_max_right.
   }
   econstructor; try eassumption.
-  assert {{ Sub m <: m0 at max i (max j k) }} by mauto using per_subtyp_cumu_left, per_subtyp_cumu_right.
-  assert (exists P El, glu_univ_elem (max i (max j k)) P El m) as [? []] by mauto using glu_univ_elem_cumu_max_left.
+  assert {{ Sub a <: a' at max i (max j k) }} by mauto using per_subtyp_cumu_left, per_subtyp_cumu_right.
+  assert (exists P El, glu_univ_elem (max i (max j k)) P El a) as [? []] by mauto using glu_univ_elem_cumu_max_left.
   eapply glu_univ_elem_per_subtyp_trm_if; mauto.
   - assert (k <= max i (max j k)) by lia.
     eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto.
   - assert (i <= max i (max j k)) by lia.
     eapply glu_univ_elem_exp_cumu_ge; mauto.
 Qed.
 
+#[export]
+Hint Resolve glu_rel_exp_subtyp : mcltt.
+
 Lemma glu_rel_sub_subtyp : forall {Γ σ Δ Δ'},
     {{ ⊩ Δ' }} ->
     {{ Γ ⊩s σ : Δ }} ->
@@ -72,5 +80,8 @@ Proof.
              end
          end; unmark_all.
   econstructor; mauto.
-  eapply glu_ctx_env_per_ctx_subtyp_sub_if; only 3: eassumption; mauto.
+  eapply glu_ctx_env_per_ctx_subtyp_sub_if; mauto.
 Qed.
+
+#[export]
+Hint Resolve glu_rel_sub_subtyp : mcltt.