diff options
| -rwxr-xr-x | doc/RefMan-cic.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex index 4fd12e0f2d..278d6d1a73 100755 --- a/doc/RefMan-cic.tex +++ b/doc/RefMan-cic.tex @@ -394,6 +394,8 @@ convertibility into an order inductively defined by: \begin{enumerate} \item if $\WTEGCONV{t}{u}$ then $\WTEGLECONV{t}{u}$, \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$, +\item for any $i$, $\Prop\WTEGLECONV\Type(i)$, +\item for any $i$, $\Set\WTEGLECONV\Type(i)$, \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{(x:T)T'}{(x:U)U'}$. \end{enumerate} |