fact: Fixpoint argument_types (B : Ast.term) := match B with | tProd _ A B => A :: argument_types B | _ => [] end.
imports: Ascii String Undecidability.L(Util.L_facts) MetaCoq(Template.All Template.Checker) Undecidability.Shared.Libs.PSL.Base MetaCoq.Utils.bytestring