fixup! wip generic typing lemmas

CoqHott · Nov 17, 2023 · 410f1cc · 410f1cc
1 parent 7f0f113
commit 410f1cc
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/theories/GenericTyping.v b/theories/GenericTyping.v
@@ -918,17 +918,17 @@ Section GenericConsequences.
 
   (** *** Derived typing, reduction and conversion judgements *)
 
-  Lemma ty_var0 {Γ A} : 
-    [Γ |- A] ->
+  Lemma ty_var0 {Γ A s} :
+    [Γ |- A @ s] ->
     [Γ ,, A |- tRel 0 : A⟨↑⟩].
   Proof. 
     intros; refine (ty_var _ (in_here _ _)); gen_typing.
   Qed.
 
   Lemma wft_simple_arr {Γ A B} :
-    [Γ |- A] ->
-    [Γ |- B] ->
-    [Γ |- arr A B].
+    [Γ |- A @ set] ->
+    [Γ |- B @ set] ->
+    [Γ |- arr A B @ set].
   Proof.
     intros. eapply wft_prod; renToWk; tea.
     eapply wft_wk; gen_typing.