Add new prototype grammar `substCandid` to fix substition parse errors

grammar.ott

@@ -206,14 +206,14 @@ es {{ tex \overline{\ottnt{[[e]]} } }} :: 'Expressions_' ::= {{ com List of expr
 % %%  Metatheory  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 theta {{ tex \theta }}, spsi {{ tex \psi }} :: 'MonoSubst_' ::= {{ com Mono Type substitutions }}
-| [ </ ai := ti // i /> ]   :: :: SubstList      {{ com Mappings }}
-| [< a := t >]              :: M :: Overline
+| [ </ substCandidi := SubstCandid'i // i /> ]   :: :: SubstList      {{ com Mappings }} 
+| [< substCandid := substCandid' >]              :: M :: Overline
   {{ tex [\overline{[[a]] [[:=]] [[t]]}] }}
 | theta1 theta2              :: M :: Concat
 
 btheta {{ tex \Theta }}, bpsi {{ tex \Psi }} :: 'PolySubst_' ::= {{ com Poly Type substitutions }}
-| [ </ kai := si // i /> ] ::   :: SubstList
-| [< ka := s >]            :: M :: Overline  {{ tex [\overline{[[ka]] [[:=]] [[s]]}] }}
+| [ </ substCandidi := substCandid'i // i /> ] ::   :: SubstList
+| [< substCandid := substCandid' >]            :: M :: Overline  {{ tex [\overline{[[ka]] [[:=]] [[s]]}] }}
 | emptyset                 ::   :: Empty     {{ com Empty set }}
 | btheta o btheta'         ::   :: Comp      {{ com Composition }}
 
@@ -270,7 +270,14 @@ substs :: SubstObject ::= {{ com Substitutions }}
 | theta  :: :: MonoSubst
 | btheta :: :: PolySubst
 
-hasInstVar :: HasInstantiationVar ::= {{ com Thigns that may contain instantiation variables }}
+substCandid :: SubstCandidate ::= {{ com Things that we can use in a substitution }}
+| ka :: :: InstVar
+| a :: :: TypeVar
+| t :: :: MonoType
+| s :: :: PolyType
+| rho :: :: RhoType
+
+hasInstVar :: HasInstantiationVar ::= {{ com Things that may contain instantiation variables }}
 | rhos        :: :: RhoTypes 
 | phs         :: :: PolyTypes 
 | ph          :: :: PolyType