fact: Fixpoint tmIsType (s : Ast.term) : TemplateMonad bool := match s with | tInd _ _ => ret true | tConst n u => t <- tmTypeOf (tConst n u) ;; match t with tSort _ => ret true | _ => ret false end | tVar x => t <- tmTypeOf (tVar x) ;; match t with tSort _ => ret true | _ => ret false end | tApp h _ => tmIsType h | _ => ret false end.
imports: Ascii String Undecidability.L(Util.L_facts) MetaCoq(Template.All Template.Checker) Undecidability.Shared.Libs.PSL.Base MetaCoq.Utils.bytestring