exploit autorewrites

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -264,12 +264,14 @@ Proof.
     edestruct H11 as [? []]; eauto.
     eexists; split; eauto.
     eapply H2; eauto.
-    assert {{ Γ ⊢ m ≈ t' : Π IT OT }} by mauto.
-    assert {{ Δ ⊢ m [ σ ] ≈ t' [ σ ] : (Π IT OT) [ σ ] }} by mauto 4.
-
-    admit.                      (* this is annoying. a simple way? *)
-
+    assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
+    assert {{ Δ ⊢ IT [ σ ] : Type @ i4 }} by mauto 3.
+    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [|mauto 4].
+    autorewrite with mcltt in Hty.
+    eapply wf_exp_eq_app_cong with (N := m') (N' := m') in Hty; try pi_univ_level_tac; [|mauto 2].
+    autorewrite with mcltt in Hty.
+    eassumption.
   - intros.
     assert {{ Δ ⊢ m [ σ ] ≈ t' [ σ ] : M [ σ ] }} by mauto 4.
     mauto.
-Admitted.
+Qed.

theories/Core/Syntactic/Corollaries.v

@@ -42,3 +42,10 @@ Add Parametric Morphism i Γ Δ : a_sub
 Proof.
   intros. gen_presups. mauto 4.
 Qed.
+
+
+Add Parametric Morphism i Γ Δ t (H : {{ Δ ⊢ t : Type@i }}) : (a_sub t)
+    with signature wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong1.
+Proof.
+  intros. gen_presups. mauto 4.
+Qed.

theories/Core/Syntactic/System/Definitions.v

@@ -338,7 +338,6 @@ Qed.
 #[export]
   Hint Rewrite -> wf_sub_eq_id_compose_right wf_sub_eq_id_compose_left
                    wf_sub_eq_compose_assoc (* prefer right association *)
-                   wf_sub_eq_extend_compose
                    wf_sub_eq_p_extend using mauto 4 : mcltt.
 
 

theories/Core/Syntactic/System/Lemmas.v

@@ -592,6 +592,8 @@ Qed.
 
 #[export]
 Hint Resolve sub_eq_q_sigma_id_extend : mcltt.
+#[export]
+ 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 : Δ }}.
 Proof with mautosolve 3.