fact: Fixpoint mkLApp (s : term) (L : list term) := match L with | [] => s | t :: L => mkLApp (tApp (tConstruct (mkInd term_kn 0) 1 []) [s; t]) L end.
imports: Undecidability.L(L Tactics.Computable Tactics.ComputableTactics Tactics.Extract) MetaCoq(Template.All TemplateMonad.Core Template.Ast) List MetaCoq.Utils.bytestring