fact: Definition split_head_symbol A : option (inductive * list term) := match A with | tApp (tInd ind u) R => Some (ind, R) | tInd ind u => Some (ind, []) | _ => None end.
imports: Ascii String Undecidability.L(Util.L_facts) MetaCoq(Template.All Template.Checker) Undecidability.Shared.Libs.PSL.Base MetaCoq.Utils.bytestring