fact: Fixpoint termsUpTo(n: nat): list term := match n with | O => [] | S m => List.map tVar (natsUpTo m) ++ List.map (fun '(A, B, body) => tLam A B body) (list_prod (list_prod (typesUpTo m) (typesUpTo m)) (termsUpTo m)) ++ List.map (fun '(t1, t2) => tApp t1 t2) (list_prod (termsUpTo m) (termsUpTo m)) ++ [tO] ++ [tS] ++ List.map tNatRec (typesUpTo m) end.
imports: Arith Lia List