- | T.Decl -> [], E.Abst (n, tt)
- | T.Ax -> [], E.Abst (n, tt)
- | T.Cong -> [], E.Abst (n, tt)
- | T.Def -> [], E.Abbr tt
- | T.Th -> [], E.Abbr tt
+ | T.Decl -> [] , E.Abst (n, tt)
+ | T.Ax -> [E.InProp] , E.Abst (n, tt)
+ | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
+ | T.Def -> [] , E.Abbr tt
+ | T.Th -> [E.InProp] , E.Abbr tt