- | T.Decl -> [] , E.Abst tt
- | T.Ax -> [E.InProp] , E.Abst tt
- | T.Cong -> [E.InProp; E.Progress], E.Abst tt
- | T.Def -> [] , E.Abbr tt
- | T.Th -> [E.InProp] , E.Abbr tt
+ | T.Decl -> [] , E.abst E.empty_env tt
+ | T.Ax -> [E.InProp] , E.abst E.empty_env tt
+ | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt
+ | T.Def -> [] , E.abbr E.empty_env tt
+ | T.Th -> [E.InProp] , E.abbr E.empty_env tt