Additional lemmas (#115)

theories/Core/Syntactic/Presup.v

@@ -260,3 +260,15 @@ Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq 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 i', {{ Γ ⊢ A : Type@i }} /\ {{ Γ ⊢ A' : Type@i' }}.
+Proof.
+  intros * H.
+  dependent induction H; gen_presups; destruct_conjs; split; mauto 4.
+  do 2 eexists; mauto 4.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_presup : mcltt.

theories/Core/Syntactic/SystemOpt.v

@@ -36,6 +36,20 @@ Hint Resolve wf_natrec' : mcltt.
 #[export]
 Remove Hints wf_natrec : mcltt.
 
+Corollary wf_pi_max : forall {Γ A i B j},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ , A ⊢ B : Type@j }} ->
+    {{ Γ ⊢ Π A B : Type@(max i j) }}.
+Proof.
+  intros.
+  assert {{ Γ ⊢ A : Type@(max i j) }} by eauto using lift_exp_max_left.
+  assert {{ Γ, A ⊢ B : Type@(max i j) }} by eauto using lift_exp_max_right.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_pi_max : mcltt.
+
 Corollary wf_fn' : forall {Γ A M B},
     {{ Γ , A ⊢ M : B }} ->
     {{ Γ ⊢ λ A M : Π A B }}.
@@ -121,6 +135,21 @@ Hint Resolve wf_exp_eq_nat_beta_succ' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_nat_beta_succ : mcltt.
 
+Corollary wf_exp_eq_pi_sub_max : forall {Γ σ Δ A i B j},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ , A ⊢ B : Type@j }} ->
+    {{ Γ ⊢ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@(max i j) }}.
+Proof.
+  intros.
+  assert {{ Δ ⊢ A : Type@(max i j) }} by eauto using lift_exp_max_left.
+  assert {{ Δ , A ⊢ B : Type@(max i j) }} by eauto using lift_exp_max_right.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_pi_sub_max : mcltt.
+
 Corollary wf_exp_eq_pi_cong' : forall {Γ A A' B B' i},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ , A ⊢ B ≈ B' : Type@i }} ->
@@ -134,6 +163,20 @@ Hint Resolve wf_exp_eq_pi_cong' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_pi_cong : mcltt.
 
+Corollary wf_exp_eq_pi_cong_max : forall {Γ A A' i B B' j},
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ , A ⊢ B ≈ B' : Type@j }} ->
+    {{ Γ ⊢ Π A B ≈ Π A' B' : Type@(max i j) }}.
+Proof.
+  intros.
+  assert {{ Γ ⊢ A ≈ A' : Type@(max i j) }} by eauto using lift_exp_eq_max_left.
+  assert {{ Γ , A ⊢ B ≈ B' : Type@(max i j) }} by eauto using lift_exp_eq_max_right.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_pi_cong_max : mcltt.
+
 Corollary wf_exp_eq_fn_cong' : forall {Γ A A' i B M M'},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ , A ⊢ M ≈ M' : B }} ->