From 6f53aca07665c45af6c1713869f5434208607188 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Thu, 31 Jan 2019 19:24:39 +0900
Subject: The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.

c can be non-function since c:U.
So, c c' is not typeable.
---
 doc/sphinx/language/cic.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index e3fd543c93..6ea3bcef23 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1766,12 +1766,12 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution
 .. math::
    \frac{\WF{E;~c:U;~E′;~c′:=t:T;~E″}{Γ}}
         {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}
-	{\subst{Γ}{c}{(c~c′)}}}
+        {\subst{Γ}{c′}{(c′~c)}}}
 
    
 .. math::
    \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}}
-        {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c}{(c~c′)}}}
+        {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}}
 	
 .. math::
    \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}}
-- 
cgit v1.2.3