Reformulate renaming

theories/structural.v

@@ -3,17 +3,11 @@ From Hammer Require Import Tactics.
 Require Import ssreflect.
 
 
-Lemma lem :
-  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
-  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> )  /\
-  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...).
-Proof. apply wt_mutual. ...
-
-
 Lemma wff_mutual :
   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ⊢ Γ)  /\
-  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ).
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ) /\
+  (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ⊢ Γ).
 Proof. apply wt_mutual; eauto. Qed.
 
 #[export]Hint Constructors Wt Wff Eq : wt.
@@ -35,7 +29,9 @@ Lemma renaming :
   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
      Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A) /\
   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
-     Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A).
+     Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A) /\
+  (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> forall  m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+    Δ ⊢ ren_PTm ξ A ≲ ren_PTm ξ B).
 Proof.
   apply wt_mutual => //=; eauto 3 with wt.
   - move => n Γ i hΓ _ m Δ ξ hΔ hξ.

theories/typing.v

@@ -105,6 +105,7 @@ with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
   Γ ⊢ A ≲ C
 
 | Su_Univ n Γ i j :
+  ⊢ Γ ->
   i <= j ->
   Γ ⊢ PUniv i : PTm n ≲ PUniv j
 
@@ -164,5 +165,6 @@ Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.
 (* Lemma lem : *)
 (*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
 (*   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...)  /\ *)
-(*   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...). *)
+(*   (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *)
+(*   (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *)
 (* Proof. apply wt_mutual. ... *)