From 842476ea78da45120de838593e004a79bac0434d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 24 Mar 2017 12:53:33 +0100
Subject: [PATCH] comment

---
 theories/typing/type.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index 401392ae..0e8fdeae 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -73,6 +73,7 @@ Proof.
     + apply IH, Hαβ. etrans; last done. by apply submseteq_cons.
 Qed.
 
+(* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
 Inductive TyWfLst `{typeG Σ} : list type → Type :=
 | tyl_wf_nil : TyWfLst []
 | tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
-- 
GitLab