content: 
  {-|
  Generating test files with code copied & renamed multiple times.
  -}
  
  module GenTestFiles where
  
  replace :: String -> String -> String
  replace x =
    foldr (\c s -> case c of '%' -> x ++ s; _ -> c:s) []
  
  render :: [String] -> Int -> String
  render ls n = replace (if n == 0 then "" else show n) $ unlines ls
  
  times :: Int -> (Int -> String) -> String
  times n f = concatMap f [0..n-1]
  
  -- todo: genEverything function
  
  smallttStlc10k       = writeFile "bench/stlc10k.stt"         $ times 80 smallttStlc
  smallttStlc5k        = writeFile "bench/stlc5k.stt"          $ times 40 smallttStlc
  smallttStlcLessImpl10k = writeFile "bench/stlc_lessimpl10k.stt"  $ times 80 smallttStlcLessImpl
  smallttStlcLessImpl5k = writeFile "bench/stlc_lessimpl5k.stt"  $ times 40 smallttStlcLessImpl
  smallttStlc100k      = writeFile "bench/stlc100k.stt"        $ times 800 smallttStlc
  
  leanStlc1k           = writeFile "bench/stlc1k.lean"         $ times 8 leanStlc
  leanStlc5k           = writeFile "bench/stlc5k.lean"         $ times 40 leanStlc
  leanStlc10k          = writeFile "bench/stlc10k.lean"        $ times 80 leanStlc
  leanStlcLessImpl10k    = writeFile "bench/stlc_lessimpl10k.lean" $ times 80 leanStlcLessImpl
  leanStlcLessImpl5k     = writeFile "bench/stlc_lessimpl5k.lean"  $ times 40 leanStlcLessImpl
  leanStlc100k         = writeFile "bench/stlc100k.lean"       $ times 800 leanStlc
  
  agdaStlcLessImpl10k    = writeFile "bench/stlc_lessimpl10k.agda" $ times 80 agdaStlcLessImpl
  agdaStlcLessImpl5k    = writeFile "bench/stlc_lessimpl5k.agda" $ times 40 agdaStlcLessImpl
  agdaStlc1k           = writeFile "bench/stlc1k.agda"         $ times 8 agdaStlc
  agdaStlc5k           = writeFile "bench/stlc5k.agda"         $ times 40 agdaStlc
  agdaStlc10k          = writeFile "bench/stlc10k.agda"        $ times 80 agdaStlc
  agdaStlc100k         = writeFile "bench/stlc100k.agda"       $ times 800 agdaStlc
  
  idrisStlc1k           = writeFile "bench/stlc1k.idr"         $ times 8 idrisStlc
  idrisStlc5k           = writeFile "bench/stlc5k.idr"         $ times 40 idrisStlc
  idrisStlc10k          = writeFile "bench/stlc10k.idr"        $ times 80 idrisStlc
  
  coqStlcLessImpl10k     = writeFile "bench/stlc_lessimpl10k.v"    $ times 80 coqStlcLessImpl
  coqStlcLessImpl5k      = writeFile "bench/stlc_lessimpl5k.v"    $ times 40 coqStlcLessImpl
  idrisStlcLessImpl10k     = writeFile "bench/stlc_lessimpl10k.idr"    $ times 80 idrisStlcLessImpl
  idrisStlcLessImpl5k      = writeFile "bench/stlc_lessimpl5k.idr"    $ times 40 idrisStlcLessImpl
  
  smallttStlcSmall10k = writeFile "bench/stlc_small10k.stt" $ times 192 smallttStlcSmall
  smallttStlcSmall5k  = writeFile "bench/stlc_small5k.stt"  $ times 96 smallttStlcSmall
  agdaStlcSmall10k = writeFile "bench/stlc_small10k.agda" $ times 192 agdaStlcSmall
  agdaStlcSmall5k  = writeFile "bench/stlc_small5k.agda"  $ times 96 agdaStlcSmall
  coqStlcSmall10k = writeFile "bench/stlc_small10k.v" $ times 192 coqStlcSmall
  coqStlcSmall5k  = writeFile "bench/stlc_small5k.v"  $ times 96 coqStlcSmall
  leanStlcSmall10k = writeFile "bench/stlc_small10k.lean" $ times 192 leanStlcSmall
  leanStlcSmall5k  = writeFile "bench/stlc_small5k.lean"  $ times 96 leanStlcSmall
  idrisStlcSmall10k = writeFile "bench/stlc_small10k.idr" $ times 192 idrisStlcSmall
  idrisStlcSmall5k  = writeFile "bench/stlc_small5k.idr"  $ times 96 idrisStlcSmall
  
  idrisStlcSmall1k  = writeFile "bench/stlc_small1k.idr"  $ times 19 idrisStlcSmall
  idrisStlcSmall2k  = writeFile "bench/stlc_small2k.idr"  $ times 38 idrisStlcSmall
  
  agdaStlcSmall1M     = writeFile "bench/stlc_small1M.agda" $ times 19200 agdaStlcSmall
  coqStlcSmall1M      = writeFile "bench/stlc_small1M.v"    $ times 19200 coqStlcSmall
  leanStlcSmall1M     = writeFile "bench/stlc_small1M.lean" $ times 19200 leanStlcSmall
  smallttStlcSmall1M  = writeFile "bench/stlc_small1M.stt"  $ times 19200 smallttStlcSmall
  idrisStlcSmall1M  = writeFile "bench/stlc_small1M.idr"  $ times 19200 idrisStlcSmall
  
  test1 :: Int -> String
  test1 = render [
    "id% : {A} → A → A",
    " = λ x. x",
    "",
    "id%Test : {A} → A → A",
    "  = id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id%",
    "    id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id% id%",
    "",
    "Nat% : U",
    " = (n : U) → (n → n) → n → n",
    "",
    "zero% : Nat%",
    " = λ n s z. z",
    "",
    "suc% : Nat% → Nat%",
    " = λ a n s z. s (a n s z)",
    "",
    "add% : Nat% → Nat% → Nat%",
    " = λ a b n s z. a n s (b n s z)",
    "",
    "mul% : Nat% → Nat% → Nat%",
    " = λ a b n s. a n (b n s)",
    "",
    "Eq% : {A} → A → A → U",
    " = λ {A} x y. (P : A → U) → P x → P y",
    "",
    "refl% : {A}{x : A} → Eq% x x",
    " = λ P px. px",
    "",
    "two%   : Nat% = λ N s z. s (s z)",
    "five%  : Nat% = λ N s z. s (s (s (s (s z))))",
    "n10%    = mul% two%  five%",
    "n10b%   = mul% five% two%",
    "n20%    = mul% two%  n10%",
    "n20b%   = mul% two%  n10b%",
    "n21%    = suc% n20%",
    "n21b%   = suc% n20b%",
    "n22%    = suc% n21%",
    "n22b%   = suc% n21b%",
    "n100%   = mul% n10%   n10%",
    "n100b%  = mul% n10b%  n10b%",
    "n10k%   = mul% n100%  n100%",
    "n10kb%  = mul% n100b% n100b%",
    "n100k%  = mul% n10k%  n10%",
    "n100kb% = mul% n10kb% n10b%",
    "n1M%    = mul% n10k%  n100%",
    "n1Mb%   = mul% n10kb% n100b%",
    "n5M%    = mul% n1M%   five%",
    "n5Mb%   = mul% n1Mb%  five%",
    "n10M%   = mul% n5M%   two%",
    "n10Mb%  = mul% n5Mb%  two%",
    "",
    "",
    "Vec% : U → Nat% → U",
    " = λ a n. (V : Nat% → U) → V zero% → ({n} → a → V n → V (suc% n)) → V n",
    "",
    "vnil% : {a} → Vec% a zero%",
    " = λ V n c. n",
    "",
    "vcons% : {a n} → a → Vec% a n → Vec% a (suc% n)",
    " = λ a as V n c. c a (as V n c)",
    "",
    "vec1% = (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero%",
    "       (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero%",
    "       (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero%",
    "       (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero%",
    "       (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero% (vcons% zero%",
    "       (vcons% zero% (vcons% zero% vnil%))))))))))))))))))))))))))))))))",
    "",
    "Pair% : U → U → U",
    " = λ A B. (Pair% : U)(pair : A → B → Pair%) → Pair%",
    "",
    "pair% : {A B} → A → B → Pair% A B",
    " = λ a b Pair% pair. pair a b",
    "",
    "proj1% : {A B} → Pair% A B → A",
    " = λ p. p _ (λ x y. x)",
    "",
    "proj2% : {A B} → Pair% A B → B",
    " = λ p. p _ (λ x y. y)",
    "",
    "Top% : U",
    " = (Top : U)(tt : Top) → Top",
    "",
    "tt% : Top%",
    " = λ Top tt. tt",
    "",
    "Bot% : U",
    " = (Bot : U) → Bot",
    "",
    "Ty% : U",
    " = (Ty  : U)",
    "   (ι   : Ty)",
    "   (fun : Ty → Ty → Ty)",
    " → Ty",
    "",
    "ι% : Ty%",
    " = λ _ ι _. ι",
    "",
    "fun% : Ty% → Ty% → Ty%",
    " = λ A B Ty ι fun. fun (A Ty ι fun) (B Ty ι fun)",
    "",
    "Con% : U",
    " = (Con : U)",
    "   (nil  : Con)",
    "   (cons : Con → Ty% → Con)",
    " → Con",
    "",
    "nil% : Con%",
    " = λ Con nil cons. nil",
    "",
    "cons% : Con% → Ty% → Con%",
    " = λ Γ A Con nil cons. cons (Γ Con nil cons) A",
    "",
    "Var% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Var : Con% → Ty% → U)",
    "   (vz  : {Γ A} → Var (cons% Γ A) A)",
    "   (vs  : {Γ B A} → Var Γ A → Var (cons% Γ B) A)",
    " → Var Γ A",
    "",
    "vz% : {Γ A} → Var% (cons% Γ A) A",
    " = λ Var vz vs. vz",
    "",
    "vs% : {Γ B A} → Var% Γ A → Var% (cons% Γ B) A",
    " = λ x Var vz vs. vs (x Var vz vs)",
    "",
    "Tm% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Tm  : Con% → Ty% → U)",
    "   (var : {Γ A} → Var% Γ A → Tm Γ A)",
    "   (lam : {Γ A B} → Tm (cons% Γ A) B → Tm Γ (fun% A B))",
    "   (app : {Γ A B} → Tm Γ (fun% A B) → Tm Γ A → Tm Γ B)",
    " → Tm Γ A",
    "",
    "var% : {Γ A} → Var% Γ A → Tm% Γ A",
    " = λ x Tm var lam app. var x",
    "",
    "lam% : {Γ A B} → Tm% (cons% Γ A) B → Tm% Γ (fun% A B)",
    " = λ t Tm var lam app. lam (t Tm var lam app)",
    "",
    "app% : {Γ A B} → Tm% Γ (fun% A B) → Tm% Γ A → Tm% Γ B",
    " = λ t u Tm var lam app. app (t Tm var lam app) (u Tm var lam app)",
    "",
    "EvalTy% : Ty% → U",
    " = λ A. A _ Bot% (λ A B. A → B)",
    "",
    "EvalCon% : Con% → U",
    " = λ Γ. Γ _ Top% (λ Δ A. Pair% Δ (EvalTy% A))",
    "",
    "EvalVar% : {Γ A} → Var% Γ A → EvalCon% Γ → EvalTy% A",
    " = λ x. x (λ Γ A. EvalCon% Γ → EvalTy% A)",
    "          (λ env. proj2% env)",
    "          (λ rec env. rec (proj1% env))",
    "",
    "EvalTm% : {Γ A} → Tm% Γ A → EvalCon% Γ → EvalTy% A",
    " = λ t. t _",
    "          EvalVar%",
    "          (λ t env α. t (pair% env α))",
    "          (λ t u env. t env (u env))",
    "",
    "test% : Tm% nil% (fun% (fun% ι% ι%) (fun% ι% ι%))",
    "  = lam% (lam% (app% (var% (vs% vz%)) (app% (var% (vs% vz%))",
    "             (app% (var% (vs% vz%)) (app% (var% (vs% vz%))",
    "             (app% (var% (vs% vz%)) (app% (var% (vs% vz%)) (var% vz%))))))))"
  
    ]
  
  smallttStlc :: Int -> String
  smallttStlc = render [
    "Ty% : U",
    " = (Ty%           : U)",
    "   (nat top bot  : Ty%)",
    "   (arr prod sum : Ty% → Ty% → Ty%)",
    " → Ty%",
    "",
    "nat% : Ty% = λ _ nat% _ _ _ _ _. nat%",
    "top% : Ty% = λ _ _ top% _ _ _ _. top%",
    "bot% : Ty% = λ _ _ _ bot% _ _ _. bot%",
    "",
    "arr% : Ty% → Ty% → Ty%",
    " = λ A B Ty% nat% top% bot% arr% prod sum.",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)",
    "",
    "prod% : Ty% → Ty% → Ty%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum.",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)",
    "",
    "sum% : Ty% → Ty% → Ty%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum%.",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)",
    "",
    "Con% : U",
    " = (Con% : U)",
    "   (nil  : Con%)",
    "   (snoc : Con% → Ty% → Con%)",
    " → Con%",
    "",
    "nil% : Con%",
    " = λ Con% nil% snoc. nil%",
    "",
    "snoc% : Con% → Ty% → Con%",
    " = λ Γ A Con% nil% snoc%. snoc% (Γ Con% nil% snoc%) A",
    "",
    "Var% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Var% : Con% → Ty% → U)",
    "   (vz  : {Γ A} → Var% (snoc% Γ A) A)",
    "   (vs  : {Γ B A} → Var% Γ A → Var% (snoc% Γ B) A)",
    " → Var% Γ A",
    "",
    "vz% : {Γ A} → Var% (snoc% Γ A) A",
    " = λ Var% vz% vs. vz%",
    "",
    "vs% : {Γ B A} → Var% Γ A → Var% (snoc% Γ B) A",
    " = λ x Var% vz% vs%. vs% (x Var% vz% vs%)",
    "",
    "Tm% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Tm%    : Con% → Ty% → U)",
    "   (var   : {Γ A} → Var% Γ A → Tm% Γ A)",
    "   (lam   : {Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "   (app   : {Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "   (tt    : {Γ} → Tm% Γ top%)",
    "   (pair  : {Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))",
    "   (fst   : {Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A)",
    "   (snd   : {Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B)",
    "   (left  : {Γ A B} → Tm% Γ A → Tm% Γ (sum% A B))",
    "   (right : {Γ A B} → Tm% Γ B → Tm% Γ (sum% A B))",
    "   (case  : {Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)",
    "   (zero  : {Γ} → Tm% Γ nat%)",
    "   (suc   : {Γ} → Tm% Γ nat% → Tm% Γ nat%)",
    "   (rec   : {Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)",
    " → Tm% Γ A",
    "",
    "var% : {Γ A} → Var% Γ A → Tm% Γ A",
    " = λ x Tm% var% lam app tt pair fst snd left right case zero suc rec.",
    "     var% x",
    "",
    "lam% : {Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)",
    " = λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec.",
    "     lam% (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)",
    "",
    "app% : {Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B",
    " = λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec.",
    "     app% (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "",
    "tt% : {Γ} → Tm% Γ top%",
    " = λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec. tt%",
    "",
    "pair% : {Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B)",
    " = λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec.",
    "     pair% (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "",
    "fst% : {Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec.",
    "     fst% (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)",
    "",
    "snd% : {Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec.",
    "     snd% (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)",
    "",
    "left% : {Γ A B} → Tm% Γ A → Tm% Γ (sum% A B)",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec.",
    "     left% (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)",
    "",
    "right% : {Γ A B} → Tm% Γ B → Tm% Γ (sum% A B)",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec.",
    "     right% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)",
    "",
    "case% : {Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec.",
    "     case% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "          (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "",
    "zero%  : {Γ} → Tm% Γ nat%",
    " = λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec. zero%",
    "",
    "suc% : {Γ} → Tm% Γ nat% → Tm% Γ nat%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec.",
    "   suc% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)",
    "",
    "rec% : {Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%.",
    "     rec% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "",
    "v0% : {Γ A} → Tm% (snoc% Γ A) A",
    " = var% vz%",
    "",
    "v1% : {Γ A B} → Tm% (snoc% (snoc% Γ A) B) A",
    " = var% (vs% vz%)",
    "",
    "v2% : {Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " = var% (vs% (vs% vz%))",
    "",
    "v3% : {Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " = var% (vs% (vs% (vs% vz%)))",
    "",
    "tbool% : Ty%",
    " = sum% top% top%",
    "",
    "true% : {Γ} → Tm% Γ tbool%",
    " = left% tt%",
    "",
    "tfalse% : {Γ} → Tm% Γ tbool%",
    " = right% tt%",
    "",
    "ifthenelse% : {Γ A} → Tm% Γ (arr% tbool% (arr% A (arr% A A)))",
    " = lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))",
    "",
    "times4% : {Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A))",
    "  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "add% : {Γ} → Tm% Γ (arr% nat% (arr% nat% nat%))",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "       (lam% v0%))",
    "",
    "mul% : {Γ} → Tm% Γ (arr% nat% (arr% nat% nat%))",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "       (lam% zero%))",
    "",
    "fact% : {Γ} → Tm% Γ (arr% nat% nat%)",
    " = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "             (suc% zero%))"
  
    ]
  
  leanStlc :: Int -> String
  leanStlc = render [
    "def Ty% : Type 1",
    " := ∀ (Ty%           : Type)",
    "      (nat top bot  : Ty%)",
    "      (arr prod sum : Ty% → Ty% → Ty%)",
    "    , Ty%",
    "",
    "def nat% : Ty% := λ _ nat% _ _ _ _ _ => nat%",
    "def top% : Ty% := λ _ _ top% _ _ _ _ => top%",
    "def bot% : Ty% := λ _ _ _ bot% _ _ _ => bot%",
    "",
    "def arr% : Ty% → Ty% → Ty%",
    " := λ A B Ty% nat% top% bot% arr% prod sum =>",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)",
    "",
    "def prod% : Ty% → Ty% → Ty%",
    " := λ A B Ty% nat% top% bot% arr% prod% sum =>",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)",
    "",
    "def sum% : Ty% → Ty% → Ty%",
    " := λ A B Ty% nat% top% bot% arr% prod% sum% =>",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)",
    "",
    "def Con% : Type 1",
    " := ∀ (Con%  : Type)",
    "      (nil  : Con%)",
    "      (snoc : Con% → Ty% → Con%)",
    "    , Con%",
    "",
    "def nil% : Con%",
    " := λ Con% nil% snoc => nil%",
    "",
    "def snoc% : Con% → Ty% → Con%",
    " := λ Γ A Con% nil% snoc% => snoc% (Γ Con% nil% snoc%) A",
    "",
    "def Var% : Con% → Ty% → Type 1",
    " := λ Γ A =>",
    "   ∀ (Var% : Con% → Ty% → Type)",
    "     (vz  : ∀{Γ A}, Var% (snoc% Γ A) A)",
    "     (vs  : ∀{Γ B A}, Var% Γ A → Var% (snoc% Γ B) A)",
    "   , Var% Γ A",
    "",
    "def vz% : ∀ {Γ A}, Var% (snoc% Γ A) A",
    " := λ Var% vz% vs => vz%",
    "",
    "def vs% : ∀ {Γ B A}, Var% Γ A → Var% (snoc% Γ B) A",
    " := λ x Var% vz% vs% => vs% (x Var% vz% vs%)",
    "",
    "def Tm% : Con% → Ty% → Type 1",
    " := λ Γ A =>",
    "   ∀ (Tm%  : Con% → Ty% → Type)",
    "     (var : ∀ {Γ A}, Var% Γ A → Tm% Γ A)",
    "     (lam : ∀ {Γ A B}, (Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)))",
    "     (app   : ∀ {Γ A B}   , Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "     (tt    : ∀ {Γ}       , Tm% Γ top%)",
    "     (pair  : ∀ {Γ A B}   , Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))",
    "     (fst   : ∀ {Γ A B}   , Tm% Γ (prod% A B) → Tm% Γ A)",
    "     (snd   : ∀ {Γ A B}   , Tm% Γ (prod% A B) → Tm% Γ B)",
    "     (left  : ∀ {Γ A B}   , Tm% Γ A → Tm% Γ (sum% A B))",
    "     (right : ∀ {Γ A B}   , Tm% Γ B → Tm% Γ (sum% A B))",
    "     (case  : ∀ {Γ A B C} , Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)",
    "     (zero  : ∀ {Γ}       , Tm% Γ nat%)",
    "     (suc   : ∀ {Γ}       , Tm% Γ nat% → Tm% Γ nat%)",
    "     (rec   : ∀ {Γ A}     , Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)",
    "   , Tm% Γ A",
    "",
    "def var% : ∀ {Γ A}, Var% Γ A → Tm% Γ A",
    " := λ x Tm% var% lam app tt pair fst snd left right case zero suc rec =>",
    "     var% x",
    "",
    "def lam% : ∀ {Γ A B} , Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)",
    " := λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec =>",
    "     lam% (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)",
    "",
    "def app% : ∀ {Γ A B} , Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B",
    " := λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec =>",
    "     app% (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "",
    "def tt% : ∀ {Γ} , Tm% Γ top%",
    " := λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec => tt%",
    "",
    "def pair% : ∀ {Γ A B} , Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B)",
    " := λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec =>",
    "     pair% (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "",
    "def fst% : ∀ {Γ A B} , Tm% Γ (prod% A B) → Tm% Γ A",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec =>",
    "     fst% (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)",
    "",
    "def snd% : ∀ {Γ A B} , Tm% Γ (prod% A B) → Tm% Γ B",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec =>",
    "     snd% (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)",
    "",
    "def left% : ∀ {Γ A B} , Tm% Γ A → Tm% Γ (sum% A B)",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec =>",
    "     left% (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)",
    "",
    "def right% : ∀ {Γ A B} , Tm% Γ B → Tm% Γ (sum% A B)",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec =>",
    "     right% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)",
    "",
    "def case% : ∀ {Γ A B C} , Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C",
    " := λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec =>",
    "     case% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "          (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "",
    "def zero%  : ∀ {Γ} , Tm% Γ nat%",
    " := λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec => zero%",
    "",
    "def suc% : ∀ {Γ} , Tm% Γ nat% → Tm% Γ nat%",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec =>",
    "   suc% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)",
    "",
    "def rec% : ∀ {Γ A} , Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A",
    " := λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec% =>",
    "     rec% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "",
    "def v0% : ∀ {Γ A}, Tm% (snoc% Γ A) A",
    " := var% vz%",
    "",
    "def v1% : ∀ {Γ A B}, Tm% (snoc% (snoc% Γ A) B) A",
    " := var% (vs% vz%)",
    "",
    "def v2% : ∀ {Γ A B C}, Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " := var% (vs% (vs% vz%))",
    "",
    "def v3% : ∀ {Γ A B C D}, Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " := var% (vs% (vs% (vs% vz%)))",
    "",
    "def tbool% : Ty%",
    " := sum% top% top%",
    "",
    "def ttrue% : ∀ {Γ}, Tm% Γ tbool%",
    " := left% tt%",
    "",
    "def tfalse% : ∀ {Γ}, Tm% Γ tbool%",
    " := right% tt%",
    "",
    "def ifthenelse% : ∀ {Γ A}, Tm% Γ (arr% tbool% (arr% A (arr% A A)))",
    " := lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))",
    "",
    "def times4% : ∀ {Γ A}, Tm% Γ (arr% (arr% A A) (arr% A A))",
    "  := lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "def add% : ∀ {Γ}, Tm% Γ (arr% nat% (arr% nat% nat%))",
    " := lam% (rec% v0%",
    "      (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "      (lam% v0%))",
    "",
    "def mul% : ∀ {Γ}, Tm% Γ (arr% nat% (arr% nat% nat%))",
    " := lam% (rec% v0%",
    "     (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "     (lam% zero%))",
    "",
    "def fact% : ∀ {Γ}, Tm% Γ (arr% nat% nat%)",
    " := lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "        (suc% zero%))"
    ]
  
  agdaStlc :: Int -> String
  agdaStlc = render [
    "{-# OPTIONS --type-in-type #-}",
    "",
    "Ty% : Set",
    "Ty% =",
    "   (Ty%         : Set)",
    "   (nat top bot  : Ty%)",
    "   (arr prod sum : Ty% → Ty% → Ty%)",
    " → Ty%",
    "",
    "nat% : Ty%; nat% = λ _ nat% _ _ _ _ _ → nat%",
    "top% : Ty%; top% = λ _ _ top% _ _ _ _ → top%",
    "bot% : Ty%; bot% = λ _ _ _ bot% _ _ _ → bot%",
    "",
    "arr% : Ty% → Ty% → Ty%; arr%",
    " = λ A B Ty% nat% top% bot% arr% prod sum →",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)",
    "",
    "prod% : Ty% → Ty% → Ty%; prod%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum →",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)",
    "",
    "sum% : Ty% → Ty% → Ty%; sum%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum% →",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)",
    "",
    "Con% : Set; Con%",
    " = (Con% : Set)",
    "   (nil  : Con%)",
    "   (snoc : Con% → Ty% → Con%)",
    " → Con%",
    "",
    "nil% : Con%; nil%",
    " = λ Con% nil% snoc → nil%",
    "",
    "snoc% : Con% → Ty% → Con%; snoc%",
    " = λ Γ A Con% nil% snoc% → snoc% (Γ Con% nil% snoc%) A",
    "",
    "Var% : Con% → Ty% → Set; Var%",
    " = λ Γ A →",
    "   (Var% : Con% → Ty% → Set)",
    "   (vz  : ∀{Γ A} → Var% (snoc% Γ A) A)",
    "   (vs  : ∀{Γ B A} → Var% Γ A → Var% (snoc% Γ B) A)",
    " → Var% Γ A",
    "",
    "vz% : ∀{Γ A} → Var% (snoc% Γ A) A; vz%",
    " = λ Var% vz% vs → vz%",
    "",
    "vs% : ∀{Γ B A} → Var% Γ A → Var% (snoc% Γ B) A; vs%",
    " = λ x Var% vz% vs% → vs% (x Var% vz% vs%)",
    "",
    "Tm% : Con% → Ty% → Set; Tm%",
    " = λ Γ A →",
    "   (Tm%  : Con% → Ty% → Set)",
    "   (var   : ∀{Γ A} → Var% Γ A → Tm% Γ A)",
    "   (lam   : ∀{Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "   (app   : ∀{Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "   (tt    : ∀{Γ} → Tm% Γ top%)",
    "   (pair  : ∀{Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))",
    "   (fst   : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A)",
    "   (snd   : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B)",
    "   (left  : ∀{Γ A B} → Tm% Γ A → Tm% Γ (sum% A B))",
    "   (right : ∀{Γ A B} → Tm% Γ B → Tm% Γ (sum% A B))",
    "   (case  : ∀{Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)",
    "   (zero  : ∀{Γ} → Tm% Γ nat%)",
    "   (suc   : ∀{Γ} → Tm% Γ nat% → Tm% Γ nat%)",
    "   (rec   : ∀{Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)",
    " → Tm% Γ A",
    "",
    "var% : ∀{Γ A} → Var% Γ A → Tm% Γ A; var%",
    " = λ x Tm% var% lam app tt pair fst snd left right case zero suc rec →",
    "     var% x",
    "",
    "lam% : ∀{Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B); lam%",
    " = λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec →",
    "     lam% (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)",
    "",
    "app% : ∀{Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B; app%",
    " = λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec →",
    "     app% (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "",
    "tt% : ∀{Γ} → Tm% Γ top%; tt%",
    " = λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec → tt%",
    "",
    "pair% : ∀{Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B); pair%",
    " = λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec →",
    "     pair% (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "",
    "fst% : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A; fst%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec →",
    "     fst% (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)",
    "",
    "snd% : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B; snd%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec →",
    "     snd% (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)",
    "",
    "left% : ∀{Γ A B} → Tm% Γ A → Tm% Γ (sum% A B); left%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec →",
    "     left% (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)",
    "",
    "right% : ∀{Γ A B} → Tm% Γ B → Tm% Γ (sum% A B); right%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec →",
    "     right% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)",
    "",
    "case% : ∀{Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C; case%",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec →",
    "     case% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "",
    "zero%  : ∀{Γ} → Tm% Γ nat%; zero%",
    " = λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec → zero%",
    "",
    "suc% : ∀{Γ} → Tm% Γ nat% → Tm% Γ nat%; suc%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec →",
    "   suc% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)",
    "",
    "rec% : ∀{Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A; rec%",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec% →",
    "     rec% (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "",
    "v0% : ∀{Γ A} → Tm% (snoc% Γ A) A; v0%",
    " = var% vz%",
    "",
    "v1% : ∀{Γ A B} → Tm% (snoc% (snoc% Γ A) B) A; v1%",
    " = var% (vs% vz%)",
    "",
    "v2% : ∀{Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A; v2%",
    " = var% (vs% (vs% vz%))",
    "",
    "v3% : ∀{Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A; v3%",
    " = var% (vs% (vs% (vs% vz%)))",
    "",
    "tbool% : Ty%; tbool%",
    " = sum% top% top%",
    "",
    "true% : ∀{Γ} → Tm% Γ tbool%; true%",
    " = left% tt%",
    "",
    "tfalse% : ∀{Γ} → Tm% Γ tbool%; tfalse%",
    " = right% tt%",
    "",
    "ifthenelse% : ∀{Γ A} → Tm% Γ (arr% tbool% (arr% A (arr% A A))); ifthenelse%",
    " = lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))",
    "",
    "times4% : ∀{Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A)); times4%",
    "  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "add% : ∀{Γ} → Tm% Γ (arr% nat% (arr% nat% nat%)); add%",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "       (lam% v0%))",
    "",
    "mul% : ∀{Γ} → Tm% Γ (arr% nat% (arr% nat% nat%)); mul%",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "       (lam% zero%))",
    "",
    "fact% : ∀{Γ} → Tm% Γ (arr% nat% nat%); fact%",
    " = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "        (suc% zero%))"
    ]
  
  smallttStlcLessImpl :: Int -> String
  smallttStlcLessImpl = render [
    "",
    "Ty% : U",
    " = (Ty%           : U)",
    "   (nat top bot  : Ty%)",
    "   (arr prod sum : Ty% → Ty% → Ty%)",
    " → Ty%",
    "",
    "nat% : Ty% = λ _ nat% _ _ _ _ _. nat%",
    "top% : Ty% = λ _ _ top% _ _ _ _. top%",
    "bot% : Ty% = λ _ _ _ bot% _ _ _. bot%",
    "",
    "arr% : Ty% → Ty% → Ty%",
    " = λ A B Ty% nat% top% bot% arr% prod sum.",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)",
    "",
    "prod% : Ty% → Ty% → Ty%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum.",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)",
    "",
    "sum% : Ty% → Ty% → Ty%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum%.",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)",
    "",
    "Con% : U",
    " = (Con% : U)",
    "   (nil  : Con%)",
    "   (snoc : Con% → Ty% → Con%)",
    " → Con%",
    "",
    "nil% : Con%",
    " = λ Con% nil% snoc. nil%",
    "",
    "snoc% : Con% → Ty% → Con%",
    " = λ Γ A Con% nil% snoc%. snoc% (Γ Con% nil% snoc%) A",
    "",
    "Var% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Var% : Con% → Ty% → U)",
    "   (vz  : (Γ : _)(A : _) → Var% (snoc% Γ A) A)",
    "   (vs  : (Γ : _)(B A : _) → Var% Γ A → Var% (snoc% Γ B) A)",
    " → Var% Γ A",
    "",
    "vz% : {Γ A} → Var% (snoc% Γ A) A",
    " = λ Var% vz% vs. vz% _ _",
    "",
    "vs% : {Γ B A} → Var% Γ A → Var% (snoc% Γ B) A",
    " = λ x Var% vz% vs%. vs% _ _ _ (x Var% vz% vs%)",
    "",
    "Tm% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Tm%    : Con% → Ty% → U)",
    "   (var   : (Γ : _) (A : _) → Var% Γ A → Tm% Γ A)",
    "   (lam   : (Γ : _) (A B : _) → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "   (app   : (Γ : _) (A B : _) → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "   (tt    : (Γ : _) → Tm% Γ top%)",
    "   (pair  : (Γ : _)(A B : _) → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))",
    "   (fst   : (Γ : _)(A B : _) → Tm% Γ (prod% A B) → Tm% Γ A)",
    "   (snd   : (Γ : _)(A B : _) → Tm% Γ (prod% A B) → Tm% Γ B)",
    "   (left  : (Γ : _)(A B : _) → Tm% Γ A → Tm% Γ (sum% A B))",
    "   (right : (Γ : _)(A B : _) → Tm% Γ B → Tm% Γ (sum% A B))",
    "   (case  : (Γ : _)(A B C : _) → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)",
    "   (zero  : (Γ : _) → Tm% Γ nat%)",
    "   (suc   : (Γ : _) → Tm% Γ nat% → Tm% Γ nat%)",
    "   (rec   : (Γ : _)(A : _) → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)",
    " → Tm% Γ A",
    "",
    "var% : {Γ A} → Var% Γ A → Tm% Γ A",
    " = λ x Tm% var% lam app tt pair fst snd left right case zero suc rec.",
    "     var% _ _ x",
    "",
    "lam% : {Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)",
    " = λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec.",
    "     lam% _ _ _ (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)",
    "",
    "app% : {Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B",
    " = λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec.",
    "     app% _ _ _ (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "                (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "",
    "tt% : {Γ} → Tm% Γ top%",
    " = λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec. tt% _",
    "",
    "pair% : {Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B)",
    " = λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec.",
    "     pair% _ _ _ (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "                 (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "",
    "fst% : {Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec.",
    "     fst% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)",
    "",
    "snd% : {Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec.",
    "     snd% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)",
    "",
    "left% : {Γ A B} → Tm% Γ A → Tm% Γ (sum% A B)",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec.",
    "     left% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)",
    "",
    "right% : {Γ A B} → Tm% Γ B → Tm% Γ (sum% A B)",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec.",
    "     right% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)",
    "",
    "case% : {Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec.",
    "     case% _ _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "          (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "",
    "zero%  : {Γ} → Tm% Γ nat%",
    " = λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec. zero% _",
    "",
    "suc% : {Γ} → Tm% Γ nat% → Tm% Γ nat%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec.",
    "   suc% _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)",
    "",
    "rec% : {Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%.",
    "     rec% _ _",
    "         (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "",
    "v0% : {Γ A} → Tm% (snoc% Γ A) A",
    " = var% vz%",
    "",
    "v1% : {Γ A B} → Tm% (snoc% (snoc% Γ A) B) A",
    " = var% (vs% vz%)",
    "",
    "v2% : {Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " = var% (vs% (vs% vz%))",
    "",
    "v3% : {Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " = var% (vs% (vs% (vs% vz%)))",
    "",
    "tbool% : Ty%",
    " = sum% top% top%",
    "",
    "true% : {Γ} → Tm% Γ tbool%",
    " = left% tt%",
    "",
    "tfalse% : {Γ} → Tm% Γ tbool%",
    " = right% tt%",
    "",
    "ifthenelse% : {Γ A} → Tm% Γ (arr% tbool% (arr% A (arr% A A)))",
    " = lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))",
    "",
    "times4% : {Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A))",
    "  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "add% : {Γ} → Tm% Γ (arr% nat% (arr% nat% nat%))",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "       (lam% v0%))",
    "",
    "mul% : {Γ} → Tm% Γ (arr% nat% (arr% nat% nat%))",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "       (lam% zero%))",
    "",
    "fact% : {Γ} → Tm% Γ (arr% nat% nat%)",
    " = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "           (suc% zero%))"
    ]
  
  leanStlcLessImpl = render [
  
    "def Ty% : Type 1",
    " := ∀ (Ty%           : Type)",
    "      (nat top bot  : Ty%)",
    "      (arr prod sum : Ty% → Ty% → Ty%)",
    "    , Ty%",
    "",
    "def nat% : Ty% := λ _ nat% _ _ _ _ _ => nat%",
    "def top% : Ty% := λ _ _ top% _ _ _ _ => top%",
    "def bot% : Ty% := λ _ _ _ bot% _ _ _ => bot%",
    "",
    "def arr% : Ty% → Ty% → Ty%",
    " := λ A B Ty% nat% top% bot% arr% prod sum =>",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)",
    "",
    "def prod% : Ty% → Ty% → Ty%",
    " := λ A B Ty% nat% top% bot% arr% prod% sum =>",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)",
    "",
    "def sum% : Ty% → Ty% → Ty%",
    " := λ A B Ty% nat% top% bot% arr% prod% sum% =>",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)",
    "",
    "def Con% : Type 1",
    " := ∀ (Con%  : Type)",
    "      (nil  : Con%)",
    "      (snoc : Con% → Ty% → Con%)",
    "    , Con%",
    "",
    "def nil% : Con%",
    " := λ Con% nil% snoc => nil%",
    "",
    "def snoc% : Con% → Ty% → Con%",
    " := λ Γ A Con% nil% snoc% => snoc% (Γ Con% nil% snoc%) A",
    "",
    "def Var% : Con% → Ty% → Type 1",
    " := λ Γ A =>",
    "   ∀ (Var% : Con% → Ty% → Type)",
    "     (vz  : ∀ Γ A, Var% (snoc% Γ A) A)",
    "     (vs  : ∀ Γ B A, Var% Γ A → Var% (snoc% Γ B) A)",
    "   , Var% Γ A",
    "",
    "def vz% : ∀ {Γ A}, Var% (snoc% Γ A) A",
    " := λ Var% vz% vs => vz% _ _",
    "",
    "def vs% : ∀ {Γ B A}, Var% Γ A → Var% (snoc% Γ B) A",
    " := λ x Var% vz% vs% => vs% _ _ _ (x Var% vz% vs%)",
    "",
    "def Tm% : Con% → Ty% → Type 1",
    " := λ Γ A =>",
    "   ∀ (Tm%  : Con% → Ty% → Type)",
    "     (var   : ∀ Γ A     , Var% Γ A → Tm% Γ A)",
    "     (lam   : ∀ Γ A B   , Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "     (app   : ∀ Γ A B   , Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "     (tt    : ∀ Γ       , Tm% Γ top%)",
    "     (pair  : ∀ Γ A B   , Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))",
    "     (fst   : ∀ Γ A B   , Tm% Γ (prod% A B) → Tm% Γ A)",
    "     (snd   : ∀ Γ A B   , Tm% Γ (prod% A B) → Tm% Γ B)",
    "     (left  : ∀ Γ A B   , Tm% Γ A → Tm% Γ (sum% A B))",
    "     (right : ∀ Γ A B   , Tm% Γ B → Tm% Γ (sum% A B))",
    "     (case  : ∀ Γ A B C , Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)",
    "     (zero  : ∀ Γ       , Tm% Γ nat%)",
    "     (suc   : ∀ Γ       , Tm% Γ nat% → Tm% Γ nat%)",
    "     (rec   : ∀ Γ A     , Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)",
    "   , Tm% Γ A",
    "",
    "def var% : ∀ {Γ A}, Var% Γ A → Tm% Γ A",
    " := λ x Tm% var% lam app tt pair fst snd left right case zero suc rec =>",
    "     var% _ _ x",
    "",
    "def lam% : ∀ {Γ A B} , Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)",
    " := λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec =>",
    "     lam% _ _ _ (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)",
    "",
    "def app% : ∀ {Γ A B} , Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B",
    " := λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec =>",
    "     app% _ _ _",
    "         (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "",
    "def tt% : ∀ {Γ} , Tm% Γ top%",
    " := λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec => tt% _",
    "",
    "def pair% : ∀ {Γ A B} , Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B)",
    " := λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec =>",
    "     pair% _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "",
    "def fst% : ∀ {Γ A B} , Tm% Γ (prod% A B) → Tm% Γ A",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec =>",
    "     fst% _ _ _",
    "         (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)",
    "",
    "def snd% : ∀ {Γ A B} , Tm% Γ (prod% A B) → Tm% Γ B",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec =>",
    "     snd% _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)",
    "",
    "def left% : ∀ {Γ A B} , Tm% Γ A → Tm% Γ (sum% A B)",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec =>",
    "     left% _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)",
    "",
    "def right% : ∀ {Γ A B} , Tm% Γ B → Tm% Γ (sum% A B)",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec =>",
    "     right% _ _ _",
    "            (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)",
    "",
    "def case% : ∀ {Γ A B C} , Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C",
    " := λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec =>",
    "     case% _ _ _ _",
    "           (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "",
    "def zero%  : ∀ {Γ} , Tm% Γ nat%",
    " := λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec => zero% _",
    "",
    "def suc% : ∀ {Γ} , Tm% Γ nat% → Tm% Γ nat%",
    " := λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec =>",
    "   suc% _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)",
    "",
    "def rec% : ∀ {Γ A} , Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A",
    " := λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec% =>",
    "     rec% _ _",
    "         (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "",
    "def v0% : ∀ {Γ A}, Tm% (snoc% Γ A) A",
    " := var% vz%",
    "",
    "def v1% : ∀ {Γ A B}, Tm% (snoc% (snoc% Γ A) B) A",
    " := var% (vs% vz%)",
    "",
    "def v2% : ∀ {Γ A B C}, Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " := var% (vs% (vs% vz%))",
    "",
    "def v3% : ∀ {Γ A B C D}, Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " := var% (vs% (vs% (vs% vz%)))",
    "",
    "def tbool% : Ty%",
    " := sum% top% top%",
    "",
    "def ttrue% : ∀ {Γ}, Tm% Γ tbool%",
    " := left% tt%",
    "",
    "def tfalse% : ∀ {Γ}, Tm% Γ tbool%",
    " := right% tt%",
    "",
    "def ifthenelse% : ∀ {Γ A}, Tm% Γ (arr% tbool% (arr% A (arr% A A)))",
    " := lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))",
    "",
    "def times4% : ∀ {Γ A}, Tm% Γ (arr% (arr% A A) (arr% A A))",
    "  := lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "def add% : ∀ {Γ}, Tm% Γ (arr% nat% (arr% nat% nat%))",
    " := lam% (rec% v0%",
    "      (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "      (lam% v0%))",
    "",
    "def mul% : ∀ {Γ}, Tm% Γ (arr% nat% (arr% nat% nat%))",
    " := lam% (rec% v0%",
    "     (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "     (lam% zero%))",
    "",
    "def fact% : ∀ {Γ}, Tm% Γ (arr% nat% nat%)",
    " := lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "(suc% zero%))"
    ]
  
  agdaStlcLessImpl = render [
  
    "{-# OPTIONS --type-in-type #-}",
    "",
    "Ty% : Set",
    "Ty% =",
    "   (Ty%         : Set)",
    "   (nat top bot  : Ty%)",
    "   (arr prod sum : Ty% → Ty% → Ty%)",
    " → Ty%",
    "",
    "nat% : Ty%; nat% = λ _ nat% _ _ _ _ _ → nat%",
    "top% : Ty%; top% = λ _ _ top% _ _ _ _ → top%",
    "bot% : Ty%; bot% = λ _ _ _ bot% _ _ _ → bot%",
    "",
    "arr% : Ty% → Ty% → Ty%; arr%",
    " = λ A B Ty% nat% top% bot% arr% prod sum →",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)",
    "",
    "prod% : Ty% → Ty% → Ty%; prod%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum →",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)",
    "",
    "sum% : Ty% → Ty% → Ty%; sum%",
    " = λ A B Ty% nat% top% bot% arr% prod% sum% →",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)",
    "",
    "Con% : Set; Con%",
    " = (Con% : Set)",
    "   (nil  : Con%)",
    "   (snoc : Con% → Ty% → Con%)",
    " → Con%",
    "",
    "nil% : Con%; nil%",
    " = λ Con% nil% snoc → nil%",
    "",
    "snoc% : Con% → Ty% → Con%; snoc%",
    " = λ Γ A Con% nil% snoc% → snoc% (Γ Con% nil% snoc%) A",
    "",
    "Var% : Con% → Ty% → Set; Var%",
    " = λ Γ A →",
    "   (Var% : Con% → Ty% → Set)",
    "   (vz  : ∀ Γ A → Var% (snoc% Γ A) A)",
    "   (vs  : ∀ Γ B A → Var% Γ A → Var% (snoc% Γ B) A)",
    " → Var% Γ A",
    "",
    "vz% : ∀{Γ A} → Var% (snoc% Γ A) A; vz%",
    " = λ Var% vz% vs → vz% _ _",
    "",
    "vs% : ∀{Γ B A} → Var% Γ A → Var% (snoc% Γ B) A; vs%",
    " = λ x Var% vz% vs% → vs% _ _ _ (x Var% vz% vs%)",
    "",
    "Tm% : Con% → Ty% → Set; Tm%",
    " = λ Γ A →",
    "   (Tm%  : Con% → Ty% → Set)",
    "   (var   : ∀ Γ A      → Var% Γ A → Tm% Γ A)",
    "   (lam   : ∀ Γ A B    → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "   (app   : ∀ Γ A B    → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "   (tt    : ∀ Γ        → Tm% Γ top%)",
    "   (pair  : ∀ Γ A B    → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))",
    "   (fst   : ∀ Γ A B    → Tm% Γ (prod% A B) → Tm% Γ A)",
    "   (snd   : ∀ Γ A B    → Tm% Γ (prod% A B) → Tm% Γ B)",
    "   (left  : ∀ Γ A B    → Tm% Γ A → Tm% Γ (sum% A B))",
    "   (right : ∀ Γ A B    → Tm% Γ B → Tm% Γ (sum% A B))",
    "   (case  : ∀ Γ A B C  → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)",
    "   (zero  : ∀ Γ        → Tm% Γ nat%)",
    "   (suc   : ∀ Γ        → Tm% Γ nat% → Tm% Γ nat%)",
    "   (rec   : ∀ Γ A      → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)",
    " → Tm% Γ A",
    "",
    "var% : ∀{Γ A} → Var% Γ A → Tm% Γ A; var%",
    " = λ x Tm% var% lam app tt pair fst snd left right case zero suc rec →",
    "     var% _ _ x",
    "",
    "lam% : ∀{Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B); lam%",
    " = λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec →",
    "     lam% _ _ _ (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)",
    "",
    "app% : ∀{Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B; app%",
    " = λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec →",
    "     app% _ _ _ (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "",
    "tt% : ∀{Γ} → Tm% Γ top%; tt%",
    " = λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec → tt% _",
    "",
    "pair% : ∀{Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B); pair%",
    " = λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec →",
    "     pair% _ _ _ (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "",
    "fst% : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A; fst%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec →",
    "     fst% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)",
    "",
    "snd% : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B; snd%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec →",
    "     snd% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)",
    "",
    "left% : ∀{Γ A B} → Tm% Γ A → Tm% Γ (sum% A B); left%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec →",
    "     left% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)",
    "",
    "right% : ∀{Γ A B} → Tm% Γ B → Tm% Γ (sum% A B); right%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec →",
    "     right% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)",
    "",
    "case% : ∀{Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C; case%",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec →",
    "     case% _ _ _ _",
    "           (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "",
    "zero%  : ∀{Γ} → Tm% Γ nat%; zero%",
    " = λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec → zero% _",
    "",
    "suc% : ∀{Γ} → Tm% Γ nat% → Tm% Γ nat%; suc%",
    " = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec →",
    "   suc% _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)",
    "",
    "rec% : ∀{Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A; rec%",
    " = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec% →",
    "     rec% _ _",
    "          (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "          (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "          (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "",
    "v0% : ∀{Γ A} → Tm% (snoc% Γ A) A; v0%",
    " = var% vz%",
    "",
    "v1% : ∀{Γ A B} → Tm% (snoc% (snoc% Γ A) B) A; v1%",
    " = var% (vs% vz%)",
    "",
    "v2% : ∀{Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A; v2%",
    " = var% (vs% (vs% vz%))",
    "",
    "v3% : ∀{Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A; v3%",
    " = var% (vs% (vs% (vs% vz%)))",
    "",
    "tbool% : Ty%; tbool%",
    " = sum% top% top%",
    "",
    "true% : ∀{Γ} → Tm% Γ tbool%; true%",
    " = left% tt%",
    "",
    "tfalse% : ∀{Γ} → Tm% Γ tbool%; tfalse%",
    " = right% tt%",
    "",
    "ifthenelse% : ∀{Γ A} → Tm% Γ (arr% tbool% (arr% A (arr% A A))); ifthenelse%",
    " = lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))",
    "",
    "times4% : ∀{Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A)); times4%",
    "  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "add% : ∀{Γ} → Tm% Γ (arr% nat% (arr% nat% nat%)); add%",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "       (lam% v0%))",
    "",
    "mul% : ∀{Γ} → Tm% Γ (arr% nat% (arr% nat% nat%)); mul%",
    " = lam% (rec% v0%",
    "       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "       (lam% zero%))",
    "",
    "fact% : ∀{Γ} → Tm% Γ (arr% nat% nat%); fact%",
    " = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "        (suc% zero%))"
    ]
  
  coqStlcLessImpl = render [
    "Definition Ty% : Set",
    " := forall (Ty% : Set)",
    "      (nat top bot  : Ty%)",
    "      (arr prod sum : Ty% -> Ty% -> Ty%)",
    "    , Ty%.",
    "",
    "Definition nat% : Ty% := fun _ nat% _ _ _ _ _ => nat%.",
    "Definition top% : Ty% := fun _ _ top% _ _ _ _ => top%.",
    "Definition bot% : Ty% := fun _ _ _ bot% _ _ _ => bot%.",
    "",
    "Definition arr% : Ty% -> Ty% -> Ty%",
    " := fun A B Ty% nat% top% bot% arr% prod sum =>",
    "     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum).",
    "",
    "Definition prod% : Ty% -> Ty% -> Ty%",
    " := fun A B Ty% nat% top% bot% arr% prod% sum =>",
    "     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum).",
    "",
    "Definition sum% : Ty% -> Ty% -> Ty%",
    " := fun A B Ty% nat% top% bot% arr% prod% sum% =>",
    "     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%).",
    "",
    "Definition Con% : Set",
    " := forall (Con%  : Set)",
    "      (nil  : Con%)",
    "      (snoc : Con% -> Ty% -> Con%)",
    "    , Con%.",
    "",
    "Definition nil% : Con%",
    " := fun Con% nil% snoc => nil%.",
    "",
    "Definition snoc% : Con% -> Ty% -> Con%",
    " := fun Γ A Con% nil% snoc% => snoc% (Γ Con% nil% snoc%) A.",
    "",
    "Definition Var% : Con% -> Ty% -> Set",
    " := fun Γ A =>",
    "   forall (Var% : Con% -> Ty% -> Set)",
    "     (vz  : forall Γ A, Var% (snoc% Γ A) A)",
    "     (vs  : forall Γ B A, Var% Γ A -> Var% (snoc% Γ B) A)",
    "   , Var% Γ A.",
    "",
    "Definition vz% {Γ A} : Var% (snoc% Γ A) A",
    " := fun Var% vz% vs => vz% _ _.",
    "",
    "Definition vs% {Γ B A} : Var% Γ A -> Var% (snoc% Γ B) A",
    " := fun x Var% vz% vs% => vs% _ _ _ (x Var% vz% vs%).",
    "",
    "Definition Tm% : Con% -> Ty% -> Set",
    " := fun Γ A =>",
    "   forall (Tm%  : Con% -> Ty% -> Set)",
    "     (var   : forall Γ A     , Var% Γ A -> Tm% Γ A)",
    "     (lam   : forall Γ A B   , Tm% (snoc% Γ A) B -> Tm% Γ (arr% A B))",
    "     (app   : forall Γ A B   , Tm% Γ (arr% A B) -> Tm% Γ A -> Tm% Γ B)",
    "     (tt    : forall Γ       , Tm% Γ top%)",
    "     (pair  : forall Γ A B   , Tm% Γ A -> Tm% Γ B -> Tm% Γ (prod% A B))",
    "     (fst   : forall Γ A B   , Tm% Γ (prod% A B) -> Tm% Γ A)",
    "     (snd   : forall Γ A B   , Tm% Γ (prod% A B) -> Tm% Γ B)",
    "     (left  : forall Γ A B   , Tm% Γ A -> Tm% Γ (sum% A B))",
    "     (right : forall Γ A B   , Tm% Γ B -> Tm% Γ (sum% A B))",
    "     (case  : forall Γ A B C , Tm% Γ (sum% A B) -> Tm% Γ (arr% A C) -> Tm% Γ (arr% B C) -> Tm% Γ C)",
    "     (zero  : forall Γ       , Tm% Γ nat%)",
    "     (suc   : forall Γ       , Tm% Γ nat% -> Tm% Γ nat%)",
    "     (rec   : forall Γ A     , Tm% Γ nat% -> Tm% Γ (arr% nat% (arr% A A)) -> Tm% Γ A -> Tm% Γ A)",
    "   , Tm% Γ A.",
    "",
    "Definition var% {Γ A} : Var% Γ A -> Tm% Γ A",
    " := fun x Tm% var% lam app tt pair fst snd left right case zero suc rec =>",
    "     var% _ _ x.",
    "",
    "Definition lam% {Γ A B} : Tm% (snoc% Γ A) B -> Tm% Γ (arr% A B)",
    " := fun t Tm% var% lam% app tt pair fst snd left right case zero suc rec =>",
    "     lam% _ _ _ (t Tm% var% lam% app tt pair fst snd left right case zero suc rec).",
    "",
    "Definition app% {Γ A B} : Tm% Γ (arr% A B) -> Tm% Γ A -> Tm% Γ B",
    " := fun t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec =>",
    "     app% _ _ _",
    "         (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)",
    "         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec).",
    "",
    "Definition tt% {Γ} : Tm% Γ top%",
    " := fun Tm% var% lam% app% tt% pair fst snd left right case zero suc rec => tt% _.",
    "",
    "Definition pair% {Γ A B} : Tm% Γ A -> Tm% Γ B -> Tm% Γ (prod% A B)",
    " := fun t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec =>",
    "     pair% _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)",
    "          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec).",
    "",
    "Definition fst% {Γ A B} : Tm% Γ (prod% A B) -> Tm% Γ A",
    " := fun t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec =>",
    "     fst% _ _ _",
    "         (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec).",
    "",
    "Definition snd% {Γ A B} : Tm% Γ (prod% A B) -> Tm% Γ B",
    " := fun t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec =>",
    "     snd% _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec).",
    "",
    "Definition left% {Γ A B} : Tm% Γ A -> Tm% Γ (sum% A B)",
    " := fun t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec =>",
    "     left% _ _ _",
    "          (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec).",
    "",
    "Definition right% {Γ A B} : Tm% Γ B -> Tm% Γ (sum% A B)",
    " := fun t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec =>",
    "     right% _ _ _",
    "            (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec).",
    "",
    "Definition case% {Γ A B C} : Tm% Γ (sum% A B) -> Tm% Γ (arr% A C) -> Tm% Γ (arr% B C) -> Tm% Γ C",
    " := fun t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec =>",
    "     case% _ _ _ _",
    "           (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)",
    "           (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec).",
    "",
    "Definition zero%  {Γ} : Tm% Γ nat%",
    " := fun Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec => zero% _.",
    "",
    "Definition suc% {Γ} : Tm% Γ nat% -> Tm% Γ nat%",
    " := fun t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec =>",
    "   suc% _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec).",
    "",
    "Definition rec% {Γ A} : Tm% Γ nat% -> Tm% Γ (arr% nat% (arr% A A)) -> Tm% Γ A -> Tm% Γ A",
    " := fun t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec% =>",
    "     rec% _ _",
    "         (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)",
    "         (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%).",
    "",
    "Definition v0% {Γ A} : Tm% (snoc% Γ A) A",
    " := var% vz%.",
    "",
    "Definition v1% {Γ A B} : Tm% (snoc% (snoc% Γ A) B) A",
    " := var% (vs% vz%).",
    "",
    "Definition v2% {Γ A B C} : Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " := var% (vs% (vs% vz%)).",
    "",
    "Definition v3% {Γ A B C D} : Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " := var% (vs% (vs% (vs% vz%))).",
    "",
    "Definition tbool% : Ty%",
    " := sum% top% top%.",
    "",
    "Definition ttrue% {Γ} : Tm% Γ tbool%",
    " := left% tt%.",
    "",
    "Definition tfalse% {Γ} : Tm% Γ tbool%",
    " := right% tt%.",
    "",
    "Definition ifthenelse% {Γ A} : Tm% Γ (arr% tbool% (arr% A (arr% A A)))",
    " := lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%)))).",
    "",
    "Definition times4% {Γ A} : Tm% Γ (arr% (arr% A A) (arr% A A))",
    "  := lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%))))).",
    "",
    "Definition add% {Γ} : Tm% Γ (arr% nat% (arr% nat% nat%))",
    " := lam% (rec% v0%",
    "      (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "      (lam% v0%)).",
    "",
    "Definition mul% {Γ} : Tm% Γ (arr% nat% (arr% nat% nat%))",
    " := lam% (rec% v0%",
    "     (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "     (lam% zero%)).",
    "",
    "Definition fact% {Γ} : Tm% Γ (arr% nat% nat%)",
    " := lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "        (suc% zero%)).",
    ""
    ]
  
  agdaStlcSmall = render [
    "{-# OPTIONS --type-in-type #-}",
    "",
    "Ty% : Set; Ty%",
    " = (Ty  : Set)",
    "   (ι   : Ty)",
    "   (arr : Ty → Ty → Ty)",
    " → Ty",
    "",
    "ι%   : Ty%; ι% = fun _ ι% _ → ι%",
    "arr% : Ty% → Ty% → Ty%; arr% = fun A B Ty% ι% arr% → arr% (A Ty% ι% arr%) (B Ty% ι% arr%)",
    "",
    "Con% : Set;Con%",
    " = (Con% : Set)",
    "   (nil  : Con%)",
    "   (snoc : Con% → Ty% → Con%)",
    " → Con%",
    "",
    "nil% : Con%;nil%",
    " = fun Con% nil% snoc → nil%",
    "",
    "snoc% : Con% → Ty% → Con%;snoc%",
    " = fun Γ A Con% nil% snoc% → snoc% (Γ Con% nil% snoc%) A",
    "",
    "Var% : Con% → Ty% → Set;Var%",
    " = fun Γ A →",
    "   (Var% : Con% → Ty% → Set)",
    "   (vz  : (Γ : _)(A : _) → Var% (snoc% Γ A) A)",
    "   (vs  : (Γ : _)(B A : _) → Var% Γ A → Var% (snoc% Γ B) A)",
    " → Var% Γ A",
    "",
    "vz% : forall{Γ A} → Var% (snoc% Γ A) A;vz%",
    " = fun Var% vz% vs → vz% _ _",
    "",
    "vs% : forall{Γ B A} → Var% Γ A → Var% (snoc% Γ B) A;vs%",
    " = fun x Var% vz% vs% → vs% _ _ _ (x Var% vz% vs%)",
    "",
    "Tm% : Con% → Ty% → Set;Tm%",
    " = fun Γ A →",
    "   (Tm%    : Con% → Ty% → Set)",
    "   (var   : (Γ : _) (A : _) → Var% Γ A → Tm% Γ A)",
    "   (lam   : (Γ : _) (A B : _) → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "   (app   : (Γ : _) (A B : _) → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    " → Tm% Γ A",
    "",
    "var% : forall{Γ A} → Var% Γ A → Tm% Γ A;var%",
    " = fun x Tm% var% lam app → var% _ _ x",
    "",
    "lam% : forall{Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B);lam%",
    " = fun t Tm% var% lam% app → lam% _ _ _ (t Tm% var% lam% app)",
    "",
    "app% : forall{Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B;app%",
    " = fun t u Tm% var% lam% app% →",
    "     app% _ _ _ (t Tm% var% lam% app%) (u Tm% var% lam% app%)",
    "",
    "v0% : forall{Γ A} → Tm% (snoc% Γ A) A;v0%",
    " = var% vz%",
    "",
    "v1% : forall{Γ A B} → Tm% (snoc% (snoc% Γ A) B) A;v1%",
    " = var% (vs% vz%)",
    "",
    "v2% : forall{Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A;v2%",
    " = var% (vs% (vs% vz%))",
    "",
    "v3% : forall{Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A;v3%",
    " = var% (vs% (vs% (vs% vz%)))",
    "",
    "v4% : forall{Γ A B C D E} → Tm% (snoc% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) E) A;v4%",
    " = var% (vs% (vs% (vs% (vs% vz%))))",
    "",
    "test% : forall{Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A));test%",
    "  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))))"
    ]
  
  smallttStlcSmall = render [
    "Ty% : U",
    " = (Ty  : U)",
    "   (ι   : Ty)",
    "   (arr : Ty → Ty → Ty)",
    " → Ty",
    "",
    "ι%   : Ty% = λ _ ι% _. ι%",
    "arr% : Ty% → Ty% → Ty% = λ A B Ty% ι% arr%. arr% (A Ty% ι% arr%) (B Ty% ι% arr%)",
    "",
    "Con% : U",
    " = (Con% : U)",
    "   (nil  : Con%)",
    "   (snoc : Con% → Ty% → Con%)",
    " → Con%",
    "",
    "nil% : Con%",
    " = λ Con% nil% snoc. nil%",
    "",
    "snoc% : Con% → Ty% → Con%",
    " = λ Γ A Con% nil% snoc%. snoc% (Γ Con% nil% snoc%) A",
    "",
    "Var% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Var% : Con% → Ty% → U)",
    "   (vz  : (Γ : _)(A : _) → Var% (snoc% Γ A) A)",
    "   (vs  : (Γ : _)(B A : _) → Var% Γ A → Var% (snoc% Γ B) A)",
    " → Var% Γ A",
    "",
    "vz% : {Γ A} → Var% (snoc% Γ A) A",
    " = λ Var% vz% vs. vz% _ _",
    "",
    "vs% : {Γ B A} → Var% Γ A → Var% (snoc% Γ B) A",
    " = λ x Var% vz% vs%. vs% _ _ _ (x Var% vz% vs%)",
    "",
    "Tm% : Con% → Ty% → U",
    " = λ Γ A.",
    "   (Tm%    : Con% → Ty% → U)",
    "   (var   : (Γ : _) (A : _) → Var% Γ A → Tm% Γ A)",
    "   (lam   : (Γ : _) (A B : _) → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "   (app   : (Γ : _) (A B : _) → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    " → Tm% Γ A",
    "",
    "var% : {Γ A} → Var% Γ A → Tm% Γ A",
    " = λ x Tm% var% lam app. var% _ _ x",
    "",
    "lam% : {Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)",
    " = λ t Tm% var% lam% app. lam% _ _ _ (t Tm% var% lam% app)",
    "",
    "app% : {Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B",
    " = λ t u Tm% var% lam% app%. ",
    "     app% _ _ _ (t Tm% var% lam% app%) (u Tm% var% lam% app%)",
    "",
    "v0% : {Γ A} → Tm% (snoc% Γ A) A",
    " = var% vz%",
    "",
    "v1% : {Γ A B} → Tm% (snoc% (snoc% Γ A) B) A",
    " = var% (vs% vz%)",
    "",
    "v2% : {Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " = var% (vs% (vs% vz%))",
    "",
    "v3% : {Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " = var% (vs% (vs% (vs% vz%)))",
    "",
    "v4% : {Γ A B C D E} → Tm% (snoc% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) E) A",
    " = var% (vs% (vs% (vs% (vs% vz%))))",
    "",
    "test% : {Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A))",
    "  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))))  "
    ]
  
  
  coqStlcSmall = render [
    "",
    "Definition Ty% : Set",
    " := forall (Ty% : Set)",
    "      (base   : Ty%)",
    "      (arr : Ty% -> Ty% -> Ty%)",
    "    , Ty%.",
    "",
    "Definition base% : Ty% := fun _ base% _ => base%.",
    "",
    "Definition arr% : Ty% -> Ty% -> Ty%",
    " := fun A B Ty% base% arr% =>",
    "     arr% (A Ty% base% arr%) (B Ty% base% arr%).",
    "",
    "Definition Con% : Set",
    " := forall (Con%  : Set)",
    "      (nil  : Con%)",
    "      (snoc : Con% -> Ty% -> Con%)",
    "    , Con%.",
    "",
    "Definition nil% : Con%",
    " := fun Con% nil% snoc => nil%.",
    "",
    "Definition snoc% : Con% -> Ty% -> Con%",
    " := fun Γ A Con% nil% snoc% => snoc% (Γ Con% nil% snoc%) A.",
    "",
    "Definition Var% : Con% -> Ty% -> Set",
    " := fun Γ A =>",
    "   forall (Var% : Con% -> Ty% -> Set)",
    "     (vz  : forall Γ A, Var% (snoc% Γ A) A)",
    "     (vs  : forall Γ B A, Var% Γ A -> Var% (snoc% Γ B) A)",
    "   , Var% Γ A.",
    "",
    "Definition vz% {Γ A} : Var% (snoc% Γ A) A",
    " := fun Var% vz% vs => vz% _ _.",
    "",
    "Definition vs% {Γ B A} : Var% Γ A -> Var% (snoc% Γ B) A",
    " := fun x Var% vz% vs% => vs% _ _ _ (x Var% vz% vs%).",
    "",
    "Definition Tm% : Con% -> Ty% -> Set",
    " := fun Γ A =>",
    "   forall (Tm%  : Con% -> Ty% -> Set)",
    "     (var   : forall Γ A     , Var% Γ A -> Tm% Γ A)",
    "     (lam   : forall Γ A B   , Tm% (snoc% Γ A) B -> Tm% Γ (arr% A B))",
    "     (app   : forall Γ A B   , Tm% Γ (arr% A B) -> Tm% Γ A -> Tm% Γ B)",
    "   , Tm% Γ A.",
    "",
    "Definition var% {Γ A} : Var% Γ A -> Tm% Γ A",
    " := fun x Tm% var% lam app =>",
    "     var% _ _ x.",
    "",
    "Definition lam% {Γ A B} : Tm% (snoc% Γ A) B -> Tm% Γ (arr% A B)",
    " := fun t Tm% var% lam% app =>",
    "     lam% _ _ _ (t Tm% var% lam% app).",
    "",
    "Definition app% {Γ A B} : Tm% Γ (arr% A B) -> Tm% Γ A -> Tm% Γ B",
    " := fun t u Tm% var% lam% app% =>",
    "     app% _ _ _",
    "         (t Tm% var% lam% app%)",
    "         (u Tm% var% lam% app%).",
    "",
    "Definition v0% {Γ A} : Tm% (snoc% Γ A) A",
    " := var% vz%.",
    "",
    "Definition v1% {Γ A B} : Tm% (snoc% (snoc% Γ A) B) A",
    " := var% (vs% vz%).",
    "",
    "Definition v2% {Γ A B C} : Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " := var% (vs% (vs% vz%)).",
    "",
    "Definition v3% {Γ A B C D} : Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " := var% (vs% (vs% (vs% vz%))).",
    "",
    "Definition v4% {Γ A B C D E} : Tm% (snoc% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) E) A",
    " := var% (vs% (vs% (vs% (vs% vz%)))).",
    "",
    "Definition test% {Γ A} : Tm% Γ (arr% (arr% A A) (arr% A A))",
    " := lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% v0%))))))).",
    ""
    ]
  
  leanStlcSmall = render [
    "",
    "def Ty% : Type 1",
    " := ∀ (Ty% : Type)",
    "      (ι   : Ty%)",
    "      (arr : Ty% → Ty% → Ty%)",
    "    , Ty%",
    "",
    "def ι% : Ty% := λ _ ι% _ => ι%",
    "",
    "def arr% : Ty% → Ty% → Ty%",
    " := λ A B Ty% ι% arr% =>",
    "     arr% (A Ty% ι% arr%) (B Ty% ι% arr%)",
    "",
    "def Con% : Type 1",
    " := ∀ (Con%  : Type)",
    "      (nil  : Con%)",
    "      (snoc : Con% → Ty% → Con%)",
    "    , Con%",
    "",
    "def nil% : Con%",
    " := λ Con% nil% snoc => nil%",
    "",
    "def snoc% : Con% → Ty% → Con%",
    " := λ Γ A Con% nil% snoc% => snoc% (Γ Con% nil% snoc%) A",
    "",
    "def Var% : Con% → Ty% → Type 1",
    " := λ Γ A =>",
    "   ∀ (Var% : Con% → Ty% → Type)",
    "     (vz  : ∀ Γ A, Var% (snoc% Γ A) A)",
    "     (vs  : ∀ Γ B A, Var% Γ A → Var% (snoc% Γ B) A)",
    "   , Var% Γ A",
    "",
    "def vz% {Γ A} : Var% (snoc% Γ A) A",
    " := λ Var% vz% vs => vz% _ _",
    "",
    "def vs% {Γ B A} : Var% Γ A → Var% (snoc% Γ B) A",
    " := λ x Var% vz% vs% => vs% _ _ _ (x Var% vz% vs%)",
    "",
    "def Tm% : Con% → Ty% → Type 1",
    " := λ Γ A =>",
    "   ∀ (Tm%  : Con% → Ty% → Type)",
    "     (var   : ∀ Γ A     , Var% Γ A → Tm% Γ A)",
    "     (lam   : ∀ Γ A B   , Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))",
    "     (app   : ∀ Γ A B   , Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)",
    "   , Tm% Γ A",
    "",
    "def var% {Γ A} : Var% Γ A → Tm% Γ A",
    " := λ x Tm% var% lam app =>",
    "     var% _ _ x",
    "",
    "def lam% {Γ A B} : Tm% (snoc% Γ A) B → Tm% Γ (arr% A B)",
    " := λ t Tm% var% lam% app =>",
    "     lam% _ _ _ (t Tm% var% lam% app)",
    "",
    "def app% {Γ A B} : Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B",
    " := λ t u Tm% var% lam% app% =>",
    "     app% _ _ _",
    "         (t Tm% var% lam% app%)",
    "         (u Tm% var% lam% app%)",
    "",
    "def v0% {Γ A} : Tm% (snoc% Γ A) A",
    " := var% vz%",
    "",
    "def v1% {Γ A B} : Tm% (snoc% (snoc% Γ A) B) A",
    " := var% (vs% vz%)",
    "",
    "def v2% {Γ A B C} : Tm% (snoc% (snoc% (snoc% Γ A) B) C) A",
    " := var% (vs% (vs% vz%))",
    "",
    "def v3% {Γ A B C D} : Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A",
    " := var% (vs% (vs% (vs% vz%)))",
    "",
    "def v4% {Γ A B C D E} : Tm% (snoc% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) E) A",
    " := var% (vs% (vs% (vs% (vs% vz%))))",
    "",
    "def test% {Γ A} : Tm% Γ (arr% (arr% A A) (arr% A A))",
    " := lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))))",
    ""
    ]
  
  
  idrisStlcSmall = render [
    "Ty% : Type",
    "Ty% = (Ty    : Type)",
    "   ->(empty : Ty)",
    "   ->(arr   : Ty -> Ty -> Ty)",
    "   -> Ty",
    "",
    "empty% : Ty%",
    "empty% = \\ _, empty, _ => empty",
    "",
    "arr% : Ty% -> Ty% -> Ty%",
    "arr% = \\ a, b, ty, empty, arr => arr (a ty empty arr) (b ty empty arr)",
    "",
    "Con% : Type",
    "Con% = (Con% : Type)",
    " ->(nil  : Con%)",
    " ->(snoc : Con% -> Ty% -> Con%)",
    " -> Con%",
    "",
    "nil% : Con%",
    "nil% = \\ con, nil%, snoc => nil%",
    "",
    "snoc% : Con% -> Ty% -> Con%",
    "snoc% = \\ g, a, con, nil%, snoc% => snoc% (g con nil% snoc%) a",
    "",
    "Var% : Con% -> Ty% -> Type",
    "Var% = \\ g, a =>",
    "    (Var% : Con% -> Ty% -> Type)",
    " -> (vz  : (g : _)-> (a : _) -> Var% (snoc% g a) a)",
    " -> (vs  : (g : _)-> (b : _) ->  (a : _) -> Var% g a -> Var% (snoc% g b) a)",
    " -> Var% g a",
    "",
    "vz% : {g : _}-> {a : _} -> Var% (snoc% g a) a",
    "vz% = \\ var, vz%, vs => vz% _ _",
    "",
    "vs% : {g : _} -> {B : _} -> {a : _} -> Var% g a -> Var% (snoc% g B) a",
    "vs% = \\ x, var, vz%, vs% => vs% _ _ _ (x var vz% vs%)",
    "",
    "Tm% : Con% -> Ty% -> Type",
    "Tm% = \\ g, a =>",
    "    (Tm%    : Con% -> Ty% -> Type)",
    " -> (var   : (g : _) -> (a : _) -> Var% g a -> Tm% g a)",
    " -> (lam   : (g : _) -> (a : _) -> (B : _) -> Tm% (snoc% g a) B -> Tm% g (arr% a B))",
    " -> (app   : (g : _) -> (a : _) -> (B : _) -> Tm% g (arr% a B) -> Tm% g a -> Tm% g B)",
    " -> Tm% g a",
    "",
    "var% : {g : _} -> {a : _} -> Var% g a -> Tm% g a",
    "var% = \\ x, tm, var%, lam, app => var% _ _ x",
    "",
    "lam% : {g : _} -> {a : _} -> {B : _} -> Tm% (snoc% g a) B -> Tm% g (arr% a B)",
    "lam% = \\ t, tm, var%, lam%, app => lam% _ _ _ (t tm var% lam% app)",
    "",
    "app% : {g:_}->{a:_}->{B:_} -> Tm% g (arr% a B) -> Tm% g a -> Tm% g B",
    "app% = \\ t, u, tm, var%, lam%, app% => app% _ _ _ (t tm var% lam% app%) (u tm var% lam% app%)",
    "",
    "v0% : {g:_}->{a:_} -> Tm% (snoc% g a) a",
    "v0% = var% vz%",
    "",
    "v1% : {g:_}->{a:_}-> {B:_}-> Tm% (snoc% (snoc% g a) B) a",
    "v1% = var% (vs% vz%)",
    "",
    "v2% : {g:_}-> {a:_}-> {B:_}-> {C:_} -> Tm% (snoc% (snoc% (snoc% g a) B) C) a",
    "v2% = var% (vs% (vs% vz%))",
    "",
    "v3% : {g:_}-> {a:_}-> {B:_}-> {C:_}-> {D:_} -> Tm% (snoc% (snoc% (snoc% (snoc% g a) B) C) D) a",
    "v3% = var% (vs% (vs% (vs% vz%)))",
    "",
    "v4% : {g:_}-> {a:_}-> {B:_}-> {C:_}-> {D:_}-> {E:_}-> Tm% (snoc% (snoc% (snoc% (snoc% (snoc% g a) B) C) D) E) a",
    "v4% = var% (vs% (vs% (vs% (vs% vz%))))",
    "",
    "test% : {g:_}-> {a:_} -> Tm% g (arr% (arr% a a) (arr% a a))",
    "test%  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))))"
    ]
  
  idrisStlc = render [
    "",
    "Ty% : Type",
    "Ty% = (Ty   : Type)",
    " ->  (nat  : Ty)",
    " ->  (top  : Ty)",
    " ->  (bot  : Ty)",
    " ->  (arr  : Ty -> Ty -> Ty)",
    " ->  (prod : Ty -> Ty -> Ty)",
    " ->  (sum  : Ty -> Ty -> Ty)",
    " ->  Ty",
    "",
    "nat% : Ty%",
    "nat% = \\ _, nat%, _, _, _, _, _ => nat%",
    "top% : Ty%",
    "top% = \\ _, _, top%, _, _, _, _ => top%",
    "bot% : Ty%",
    "bot% = \\ _, _, _, bot%, _, _, _ => bot%",
    "",
    "arr% : Ty%-> Ty%-> Ty%",
    "arr% = \\ a, b, ty, nat%, top%, bot%, arr%, prod, sum =>",
    "     arr% (a ty nat% top% bot% arr% prod sum) (b ty nat% top% bot% arr% prod sum)",
    "",
    "prod% : Ty%-> Ty%-> Ty%",
    "prod% = \\ a, b, ty, nat%, top%, bot%, arr%, prod%, sum =>",
    "     prod% (a ty nat% top% bot% arr% prod% sum) (b ty nat% top% bot% arr% prod% sum)",
    "",
    "sum% : Ty%-> Ty%-> Ty%",
    "sum% = \\ a, b, ty, nat%, top%, bot%, arr%, prod%, sum% =>",
    "     sum% (a ty nat% top% bot% arr% prod% sum%) (b ty nat% top% bot% arr% prod% sum%)",
    "",
    "Con% : Type",
    "Con% = (Con% : Type)",
    " -> (nil  : Con%)",
    " -> (snoc : Con% -> Ty%-> Con%)",
    " -> Con%",
    "",
    "nil% : Con%",
    "nil% = \\ con, nil%, snoc => nil%",
    "",
    "snoc% : Con% -> Ty%-> Con%",
    "snoc% = \\ g, a, con, nil%, snoc% => snoc% (g con nil% snoc%) a",
    "",
    "Var% : Con% -> Ty%-> Type",
    "Var% = \\ g, a =>",
    "    (Var% : Con% -> Ty%-> Type)",
    " -> (vz  : {g:_}->{a:_} -> Var% (snoc% g a) a)",
    " -> (vs  : {g:_}->{b:_}->{a:_} -> Var% g a -> Var% (snoc% g b) a)",
    " -> Var% g a",
    "",
    "vz% : {g:_}->{a:_} -> Var% (snoc% g a) a",
    "vz% = \\ var, vz%, vs => vz%",
    "",
    "vs% : {g:_}->{b:_}->{a:_} -> Var% g a -> Var% (snoc% g b) a",
    "vs% = \\ x, var, vz%, vs% => vs% (x var vz% vs%)",
    "",
    "Tm% : Con% -> Ty%-> Type",
    "Tm% = \\ g, a =>",
    "    (Tm%    : Con% -> Ty%-> Type)",
    " -> (var   : {g:_}->{a:_}-> Var% g a -> Tm% g a)",
    " -> (lam   : {g:_}->{a:_}->{b:_} -> Tm% (snoc% g a) b -> Tm% g (arr% a b))",
    " -> (app   : {g:_}->{a:_}->{b:_} -> Tm% g (arr% a b) -> Tm% g a -> Tm% g b)",
    " -> (tt    : {g:_}-> Tm% g top%)",
    " -> (pair  : {g:_}->{a:_}->{b:_} -> Tm% g a -> Tm% g b -> Tm% g (prod% a b))",
    " -> (fst   : {g:_}->{a:_}->{b:_} -> Tm% g (prod% a b) -> Tm% g a)",
    " -> (snd   : {g:_}->{a:_}->{b:_} -> Tm% g (prod% a b) -> Tm% g b)",
    " -> (left  : {g:_}->{a:_}->{b:_} -> Tm% g a -> Tm% g (sum% a b))",
    " -> (right : {g:_}->{a:_}->{b:_} -> Tm% g b -> Tm% g (sum% a b))",
    " -> (split : {g:_}->{a:_}->{b:_}-> {c:_} -> Tm% g (sum% a b) -> Tm% g (arr% a c) -> Tm% g (arr% b c) -> Tm% g c)",
    " -> (zero  : {g:_}-> Tm% g nat%)",
    " -> (suc   : {g:_}-> Tm% g nat% -> Tm% g nat%)",
    " -> (rec   : {g:_}->{a:_} -> Tm% g nat% -> Tm% g (arr% nat% (arr% a a)) -> Tm% g a -> Tm% g a)",
    " -> Tm% g a",
    "",
    "var% : {g:_}->{a:_} -> Var% g a -> Tm% g a",
    "var% = \\ x, tm, var%, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec => var% x",
    "",
    "lam% : {g:_}->{a:_}->{b:_}-> Tm% (snoc% g a) b -> Tm% g (arr% a b)",
    "lam% = \\ t, tm, var%, lam%, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>",
    "     lam% (t tm var% lam% app tt pair fst snd left right split zero suc rec)",
    "",
    "app% : {g:_}->{a:_}->{b:_} -> Tm% g (arr% a b) -> Tm% g a -> Tm% g b",
    "app% = \\ t, u, tm, var%, lam%, app%, tt, pair, fst, snd, left, right, split, zero, suc, rec =>",
    "     app% (t tm var% lam% app% tt pair fst snd left right split zero suc rec)",
    "         (u tm var% lam% app% tt pair fst snd left right split zero suc rec)",
    "",
    "tt% : {g:_} -> Tm% g Main.top%",
    "tt% = \\ tm, var%, lam%, app%, tt%, pair, fst, snd, left, right, split, zero, suc, rec => tt%",
    "",
    "pair% : {g:_}->{a:_}->{b:_} -> Tm% g a -> Tm% g b -> Tm% g (prod% a b)",
    "pair% = \\ t, u, tm, var%, lam%, app%, tt%, pair%, fst, snd, left, right, split, zero, suc, rec =>",
    "     pair% (t tm var% lam% app% tt% pair% fst snd left right split zero suc rec)",
    "          (u tm var% lam% app% tt% pair% fst snd left right split zero suc rec)",
    "",
    "fst% : {g:_}->{a:_}->{b:_}-> Tm% g (prod% a b) -> Tm% g a",
    "fst% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd, left, right, split, zero, suc, rec =>",
    "     fst% (t tm var% lam% app% tt% pair% fst% snd left right split zero suc rec)",
    "",
    "snd% : {g:_}->{a:_}->{b:_} -> Tm% g (prod% a b) -> Tm% g b",
    "snd% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left, right, split, zero, suc, rec =>",
    "     snd% (t tm var% lam% app% tt% pair% fst% snd% left right split zero suc rec)",
    "",
    "left% : {g:_}->{a:_}->{b:_} -> Tm% g a -> Tm% g (sum% a b)",
    "left% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right, split, zero, suc, rec =>",
    "     left% (t tm var% lam% app% tt% pair% fst% snd% left% right split zero suc rec)",
    "",
    "right% : {g:_}->{a:_}->{b:_} -> Tm% g b -> Tm% g (sum% a b)",
    "right% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split, zero, suc, rec =>",
    "     right% (t tm var% lam% app% tt% pair% fst% snd% left% right% split zero suc rec)",
    "",
    "split% : {g:_}->{a:_}->{b:_}->{c:_} -> Tm% g (sum% a b) -> Tm% g (arr% a c) -> Tm% g (arr% b c) -> Tm% g c",
    "split% = \\ t, u, v, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero, suc, rec =>",
    "     split% (t tm var% lam% app% tt% pair% fst% snd% left% right% split% zero suc rec)",
    "          (u tm var% lam% app% tt% pair% fst% snd% left% right% split% zero suc rec)",
    "          (v tm var% lam% app% tt% pair% fst% snd% left% right% split% zero suc rec)",
    "",
    "zero% : {g:_} -> Tm% g Main.nat%",
    "zero% = \\ tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero%, suc, rec => zero%",
    "",
    "suc% : {g:_} -> Tm% g Main.nat% -> Tm% g Main.nat%",
    "suc% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero%, suc%, rec =>",
    "   suc% (t tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec)",
    "",
    "rec% : {g:_}->{a:_} -> Tm% g Main.nat% -> Tm% g (arr% Main.nat% (arr% a a)) -> Tm% g a -> Tm% g a",
    "rec% = \\ t, u, v, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero%, suc%, rec% =>",
    "     rec% (t tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec%)",
    "         (u tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec%)",
    "         (v tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec%)",
    "",
    "v0% : {g:_}->{a:_} -> Tm% (snoc% g a) a",
    "v0% = var% vz%",
    "",
    "v1% : {g:_}->{a:_}->{b:_} -> Tm% (snoc% (snoc% g a) b) a",
    "v1% = var% (vs% vz%)",
    "",
    "v2% : {g:_}->{a:_}->{b:_}->{c:_} -> Tm% (snoc% (snoc% (snoc% g a) b) c) a",
    "v2% = var% (vs% (vs% vz%))",
    "",
    "v3% : {g:_}->{a:_}->{b:_}->{c:_}->{d:_} -> Tm% (snoc% (snoc% (snoc% (snoc% g a) b) c) d) a",
    "v3% = var% (vs% (vs% (vs% vz%)))",
    "",
    "tbool% : Ty%",
    "tbool% = sum% top% top%",
    "",
    "ttrue% : {g:_} -> Tm% g Main.tbool%",
    "ttrue% = left% tt%",
    "",
    "tfalse% : {g:_} -> Tm% g Main.tbool%",
    "tfalse% = right% tt%",
    "",
    "ifthenelse% : {g:_}->{a:_} -> Tm% g (arr% Main.tbool% (arr% a (arr% a a)))",
    "ifthenelse% = lam% (lam% (lam% (split% v2% (lam% v2%) (lam% v1%))))",
    "",
    "times4% : {g:_}->{a:_} -> Tm% g (arr% (arr% a a) (arr% a a))",
    "times4%  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "add% : {g:_} -> Tm% g (arr% Main.nat% (arr% Main.nat% Main.nat%))",
    "add% = lam% (rec% v0%",
    "       (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "       (lam% v0%))",
    "",
    "mul% : {g:_} -> Tm% g (arr% Main.nat% (arr% Main.nat% Main.nat%))",
    "mul% = lam% (rec% v0%",
    "       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "       (lam% zero%))",
    "",
    "fact% : {g:_} -> Tm% g (arr% Main.nat% Main.nat%)",
    "fact% = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "                 (suc% zero%))"
    ]
  
  idrisStlcLessImpl = render [
    "",
    "Ty% : Type",
    "Ty% = (Ty   : Type)",
    " ->  (nat  : Ty)",
    " ->  (top  : Ty)",
    " ->  (bot  : Ty)",
    " ->  (arr  : Ty -> Ty -> Ty)",
    " ->  (prod : Ty -> Ty -> Ty)",
    " ->  (sum  : Ty -> Ty -> Ty)",
    " ->  Ty",
    "",
    "nat% : Ty%",
    "nat% = \\ _, nat%, _, _, _, _, _ => nat%",
    "top% : Ty%",
    "top% = \\ _, _, top%, _, _, _, _ => top%",
    "bot% : Ty%",
    "bot% = \\ _, _, _, bot%, _, _, _ => bot%",
    "",
    "arr% : Ty%-> Ty%-> Ty%",
    "arr% = \\ a, b, ty, nat%, top%, bot%, arr%, prod, sum =>",
    "     arr% (a ty nat% top% bot% arr% prod sum) (b ty nat% top% bot% arr% prod sum)",
    "",
    "prod% : Ty%-> Ty%-> Ty%",
    "prod% = \\ a, b, ty, nat%, top%, bot%, arr%, prod%, sum =>",
    "     prod% (a ty nat% top% bot% arr% prod% sum) (b ty nat% top% bot% arr% prod% sum)",
    "",
    "sum% : Ty%-> Ty%-> Ty%",
    "sum% = \\ a, b, ty, nat%, top%, bot%, arr%, prod%, sum% =>",
    "     sum% (a ty nat% top% bot% arr% prod% sum%) (b ty nat% top% bot% arr% prod% sum%)",
    "",
    "Con% : Type",
    "Con% = (Con% : Type)",
    " -> (nil  : Con%)",
    " -> (snoc : Con% -> Ty%-> Con%)",
    " -> Con%",
    "",
    "nil% : Con%",
    "nil% = \\ con, nil%, snoc => nil%",
    "",
    "snoc% : Con% -> Ty%-> Con%",
    "snoc% = \\ g, a, con, nil%, snoc% => snoc% (g con nil% snoc%) a",
    "",
    "Var% : Con% -> Ty%-> Type",
    "Var% = \\ g, a =>",
    "    (Var% : Con% -> Ty%-> Type)",
    " -> (vz  : (g:_)->(a:_) -> Var% (snoc% g a) a)",
    " -> (vs  : (g:_)->(b:_)->(a:_) -> Var% g a -> Var% (snoc% g b) a)",
    " -> Var% g a",
    "",
    "vz% : {g:_}->{a:_} -> Var% (snoc% g a) a",
    "vz% = \\ var, vz%, vs => vz% _ _",
    "",
    "vs% : {g:_}->{b:_}->{a:_} -> Var% g a -> Var% (snoc% g b) a",
    "vs% = \\ x, var, vz%, vs% => vs% _ _ _ (x var vz% vs%)",
    "",
    "Tm% : Con% -> Ty%-> Type",
    "Tm% = \\ g, a =>",
    "    (Tm%    : Con% -> Ty%-> Type)",
    " -> (var   : (g:_)->(a:_)-> Var% g a -> Tm% g a)",
    " -> (lam   : (g:_)->(a:_)->(b:_) -> Tm% (snoc% g a) b -> Tm% g (arr% a b))",
    " -> (app   : (g:_)->(a:_)->(b:_) -> Tm% g (arr% a b) -> Tm% g a -> Tm% g b)",
    " -> (tt    : (g:_)-> Tm% g top%)",
    " -> (pair  : (g:_)->(a:_)->(b:_) -> Tm% g a -> Tm% g b -> Tm% g (prod% a b))",
    " -> (fst   : (g:_)->(a:_)->(b:_) -> Tm% g (prod% a b) -> Tm% g a)",
    " -> (snd   : (g:_)->(a:_)->(b:_) -> Tm% g (prod% a b) -> Tm% g b)",
    " -> (left  : (g:_)->(a:_)->(b:_) -> Tm% g a -> Tm% g (sum% a b))",
    " -> (right : (g:_)->(a:_)->(b:_) -> Tm% g b -> Tm% g (sum% a b))",
    " -> (split : (g:_)->(a:_)->(b:_)-> (c:_) -> Tm% g (sum% a b) -> Tm% g (arr% a c) -> Tm% g (arr% b c) -> Tm% g c)",
    " -> (zero  : (g:_)-> Tm% g nat%)",
    " -> (suc   : (g:_)-> Tm% g nat% -> Tm% g nat%)",
    " -> (rec   : (g:_)->(a:_) -> Tm% g nat% -> Tm% g (arr% nat% (arr% a a)) -> Tm% g a -> Tm% g a)",
    " -> Tm% g a",
    "",
    "var% : {g:_}->{a:_} -> Var% g a -> Tm% g a",
    "var% = \\ x, tm, var%, lam, app, tt, pair, fst, snd, left, right, split, zero, suc, rec => var% _ _ x",
    "",
    "lam% : {g:_}->{a:_}->{b:_}-> Tm% (snoc% g a) b -> Tm% g (arr% a b)",
    "lam% = \\ t, tm, var%, lam%, app, tt, pair, fst, snd, left, right, split, zero, suc, rec =>",
    "     lam% _ _ _ (t tm var% lam% app tt pair fst snd left right split zero suc rec)",
    "",
    "app% : {g:_}->{a:_}->{b:_} -> Tm% g (arr% a b) -> Tm% g a -> Tm% g b",
    "app% = \\ t, u, tm, var%, lam%, app%, tt, pair, fst, snd, left, right, split, zero, suc, rec =>",
    "     app% _ _ _ (t tm var% lam% app% tt pair fst snd left right split zero suc rec)",
    "                (u tm var% lam% app% tt pair fst snd left right split zero suc rec)",
    "",
    "tt% : {g:_} -> Tm% g Main.top%",
    "tt% = \\ tm, var%, lam%, app%, tt%, pair, fst, snd, left, right, split, zero, suc, rec => tt% _",
    "",
    "pair% : {g:_}->{a:_}->{b:_} -> Tm% g a -> Tm% g b -> Tm% g (prod% a b)",
    "pair% = \\ t, u, tm, var%, lam%, app%, tt%, pair%, fst, snd, left, right, split, zero, suc, rec =>",
    "     pair% _ _ _ (t tm var% lam% app% tt% pair% fst snd left right split zero suc rec)",
    "                 (u tm var% lam% app% tt% pair% fst snd left right split zero suc rec)",
    "",
    "fst% : {g:_}->{a:_}->{b:_}-> Tm% g (prod% a b) -> Tm% g a",
    "fst% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd, left, right, split, zero, suc, rec =>",
    "     fst% _ _ _ (t tm var% lam% app% tt% pair% fst% snd left right split zero suc rec)",
    "",
    "snd% : {g:_}->{a:_}->{b:_} -> Tm% g (prod% a b) -> Tm% g b",
    "snd% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left, right, split, zero, suc, rec =>",
    "     snd% _ _ _ (t tm var% lam% app% tt% pair% fst% snd% left right split zero suc rec)",
    "",
    "left% : {g:_}->{a:_}->{b:_} -> Tm% g a -> Tm% g (sum% a b)",
    "left% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right, split, zero, suc, rec =>",
    "     left% _ _ _ (t tm var% lam% app% tt% pair% fst% snd% left% right split zero suc rec)",
    "",
    "right% : {g:_}->{a:_}->{b:_} -> Tm% g b -> Tm% g (sum% a b)",
    "right% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split, zero, suc, rec =>",
    "     right% _ _ _ (t tm var% lam% app% tt% pair% fst% snd% left% right% split zero suc rec)",
    "",
    "split% : {g:_}->{a:_}->{b:_}->{c:_} -> Tm% g (sum% a b) -> Tm% g (arr% a c) -> Tm% g (arr% b c) -> Tm% g c",
    "split% = \\ t, u, v, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero, suc, rec =>",
    "     split% _ _ _ _",
    "          (t tm var% lam% app% tt% pair% fst% snd% left% right% split% zero suc rec)",
    "          (u tm var% lam% app% tt% pair% fst% snd% left% right% split% zero suc rec)",
    "          (v tm var% lam% app% tt% pair% fst% snd% left% right% split% zero suc rec)",
    "",
    "zero% : {g:_} -> Tm% g Main.nat%",
    "zero% = \\ tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero%, suc, rec =>",
    "  zero% _",
    "",
    "suc% : {g:_} -> Tm% g Main.nat% -> Tm% g Main.nat%",
    "suc% = \\ t, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero%, suc%, rec =>",
    "   suc% _ (t tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec)",
    "",
    "rec% : {g:_}->{a:_} -> Tm% g Main.nat% -> Tm% g (arr% Main.nat% (arr% a a)) -> Tm% g a -> Tm% g a",
    "rec% = \\ t, u, v, tm, var%, lam%, app%, tt%, pair%, fst%, snd%, left%, right%, split%, zero%, suc%, rec% =>",
    "     rec% _ _",
    "       (t tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec%)",
    "       (u tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec%)",
    "       (v tm var% lam% app% tt% pair% fst% snd% left% right% split% zero% suc% rec%)",
    "",
    "v0% : {g:_}->{a:_} -> Tm% (snoc% g a) a",
    "v0% = var% vz%",
    "",
    "v1% : {g:_}->{a:_}->{b:_} -> Tm% (snoc% (snoc% g a) b) a",
    "v1% = var% (vs% vz%)",
    "",
    "v2% : {g:_}->{a:_}->{b:_}->{c:_} -> Tm% (snoc% (snoc% (snoc% g a) b) c) a",
    "v2% = var% (vs% (vs% vz%))",
    "",
    "v3% : {g:_}->{a:_}->{b:_}->{c:_}->{d:_} -> Tm% (snoc% (snoc% (snoc% (snoc% g a) b) c) d) a",
    "v3% = var% (vs% (vs% (vs% vz%)))",
    "",
    "tbool% : Ty%",
    "tbool% = sum% top% top%",
    "",
    "ttrue% : {g:_} -> Tm% g Main.tbool%",
    "ttrue% = left% tt%",
    "",
    "tfalse% : {g:_} -> Tm% g Main.tbool%",
    "tfalse% = right% tt%",
    "",
    "ifthenelse% : {g:_}->{a:_} -> Tm% g (arr% Main.tbool% (arr% a (arr% a a)))",
    "ifthenelse% = lam% (lam% (lam% (split% v2% (lam% v2%) (lam% v1%))))",
    "",
    "times4% : {g:_}->{a:_} -> Tm% g (arr% (arr% a a) (arr% a a))",
    "times4%  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))",
    "",
    "add% : {g:_} -> Tm% g (arr% Main.nat% (arr% Main.nat% Main.nat%))",
    "add% = lam% (rec% v0%",
    "       (lam% (lam% (lam% (suc% (app% v1% v0%)))))",
    "       (lam% v0%))",
    "",
    "mul% : {g:_} -> Tm% g (arr% Main.nat% (arr% Main.nat% Main.nat%))",
    "mul% = lam% (rec% v0%",
    "       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))",
    "       (lam% zero%))",
    "",
    "fact% : {g:_} -> Tm% g (arr% Main.nat% Main.nat%)",
    "fact% = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))",
    "                 (suc% zero%))"
    ]
  