From 2a5edc8ab15e556c6ee1741ffefb6869736feada Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 13:09:32 +0100
Subject: COMMENT: question

---
 doc/refman/RefMan-cic.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 14a5e12fc5..ea1be67ee9 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1094,6 +1094,7 @@ $P_l$ arity implies $P'_l$ arity since $\WTEGLECONV{P'_l}{ \subst{P_l}{p_u}{q_u}
 we have $(\WTE{\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots  n}$;
 \item the sorts are such that all eliminations, to {\Prop}, {\Set} and
   $\Type(j)$, are allowed (see section~\ref{elimdep}).
+% QUESTION: How should I interpret the above side-condition, when I am trying to show that 'list nat : Set'?
 \end{itemize}
 \end{description}
 
-- 
cgit v1.2.3