content: -- Generated by src/templates/TemplatesCompiler
  {-# LANGUAGE OverloadedStrings #-}
  module Templates where
  import CedilleTypes
  import qualified Data.Text
  
  
  -- src/templates/Mendler.ced
  templateMendler = Module [] "1" "8" "Mendler" [Param "16" True "17" "Indices" (Tkk (KdStar "27")) "29"] [CmdDef Nothing (DefType "32" "Sigma" (KdAbs "40" "42" "A" (Tkk (KdStar "46")) (KdArrow (Tkk (KdParens "49" (KdArrow (Tkt (TpVar "50" "A")) (KdStar "54")) "56")) (KdStar "59"))) (TpLam "63" "65" "A" (Tkk (KdStar "69")) (TpLam "72" "74" "B" (Tkk (KdArrow (Tkt (TpVar "78" "A")) (KdStar "82"))) (TpIota "87" "89" "x" (TpEq "93" (Beta "94" Nothing Nothing) (Beta "98" Nothing Nothing) "100") (TpAbs "102" True "104" "X" (Tkk (KdArrow (Tkt (TpEq "108" (Beta "109" Nothing Nothing) (Beta "113" Nothing Nothing) "115")) (KdStar "118"))) (TpArrow (TpParens "121" (TpAbs "122" False "124" "a" (Tkt (TpVar "128" "A")) (TpAbs "131" False "133" "b" (Tkt (TpAppt (TpVar "137" "B") (Var "139" "a"))) (TpAppt (TpVar "142" "X") (Beta "144" Nothing (Just (PosTerm (Lam "146" False "148" "f" Nothing (App (App (Var "151" "f") False (Var "153" "a")) False (Var "155" "b"))) "157")))))) "158") False (TpAppt (TpVar "161" "X") (Var "163" "x")))))))) "165",CmdDef Nothing (DefType "166" "Product" (KdArrow (Tkk (KdStar "176")) (KdArrow (Tkk (KdStar "180")) (KdStar "184"))) (TpLam "188" "190" "A" (Tkk (KdStar "194")) (TpLam "197" "199" "B" (Tkk (KdStar "203")) (TpApp (TpApp (TpVar "206" "Sigma") (TpVar "214" "A")) (TpParens "218" (TpLam "219" "221" "_" (Tkt (TpVar "225" "A")) (TpVar "228" "B")) "230"))))) "231",CmdDef Nothing (DefTerm "233" "sigma" (Just (TpAbs "241" True "243" "A" (Tkk (KdStar "247")) (TpAbs "250" True "252" "B" (Tkk (KdArrow (Tkt (TpVar "256" "A")) (KdStar "260"))) (TpAbs "263" False "265" "a" (Tkt (TpVar "269" "A")) (TpArrow (TpAppt (TpVar "272" "B") (Var "274" "a")) False (TpApp (TpApp (TpVar "278" "Sigma") (TpVar "286" "A")) (TpVar "290" "B"))))))) (Lam "296" True "298" "A" Nothing (Lam "301" True "303" "B" Nothing (Lam "306" False "308" "a" Nothing (Lam "311" False "313" "b" Nothing (IotaPair "316" (Beta "317" Nothing (Just (PosTerm (Lam "319" False "321" "f" Nothing (App (App (Var "324" "f") False (Var "326" "a")) False (Var "328" "b"))) "330"))) (Lam "332" True "334" "X" Nothing (Lam "337" False "339" "f" Nothing (App (App (Var "342" "f") False (Var "344" "a")) False (Var "346" "b")))) Nothing "348")))))) "349",CmdDef Nothing (DefTerm "351" "SigmaInd" (Just (TpAbs "366" True "368" "A" (Tkk (KdStar "372")) (TpAbs "379" True "381" "B" (Tkk (KdArrow (Tkt (TpVar "385" "A")) (KdStar "389"))) (TpAbs "396" False "398" "x" (Tkt (TpApp (TpApp (TpVar "402" "Sigma") (TpVar "410" "A")) (TpVar "414" "B"))) (TpAbs "421" True "423" "Q" (Tkk (KdArrow (Tkt (TpApp (TpApp (TpVar "427" "Sigma") (TpVar "435" "A")) (TpVar "439" "B"))) (KdStar "443"))) (TpArrow (TpParens "450" (TpAbs "451" False "453" "a" (Tkt (TpVar "457" "A")) (TpAbs "460" False "462" "b" (Tkt (TpAppt (TpVar "466" "B") (Var "468" "a"))) (TpAppt (TpVar "471" "Q") (Parens "473" (App (App (AppTp (AppTp (Var "474" "sigma") (TpVar "482" "A")) (TpVar "486" "B")) False (Var "488" "a")) False (Var "490" "b")) "492")))) "493") False (TpAppt (TpVar "500" "Q") (Var "502" "x")))))))) (Lam "508" True "510" "A" Nothing (Lam "513" True "515" "B" Nothing (Lam "518" False "520" "x" Nothing (Lam "523" True "525" "Q" Nothing (Lam "528" False "530" "f" Nothing (App (App (App (AppTp (IotaProj (Var "537" "x") "2" "540") (TpParens "543" (TpLam "544" "546" "x" (Tkt (TpEq "550" (Beta "551" Nothing Nothing) (Beta "555" Nothing Nothing) "557")) (TpAbs "559" True "561" "x'" (Tkt (TpApp (TpApp (TpVar "566" "Sigma") (TpVar "574" "A")) (TpVar "578" "B"))) (TpArrow (TpEq "581" (Var "582" "x'") (Var "587" "x") "589") True (TpAppt (TpVar "592" "Q") (Var "594" "x'"))))) "597")) False (Parens "604" (Lam "605" False "607" "a" Nothing (Lam "610" False "612" "b" Nothing (Lam "615" True "617" "x'" Nothing (Lam "621" True "623" "e" Nothing (Rho "626" False Nothing (Var "628" "e") Nothing (App (App (Var "632" "f") False (Var "634" "a")) False (Var "636" "b"))))))) "638")) True (Var "640" "x")) True (Beta "643" Nothing Nothing)))))))) "645",CmdDef Nothing (DefTerm "647" "fst" (Just (TpAbs "653" True "655" "A" (Tkk (KdStar "659")) (TpAbs "662" True "664" "B" (Tkk (KdArrow (Tkt (TpVar "668" "A")) (KdStar "672"))) (TpArrow (TpApp (TpApp (TpVar "675" "Sigma") (TpVar "683" "A")) (TpVar "687" "B")) False (TpVar "691" "A"))))) (Lam "695" True "697" "A" Nothing (Lam "700" True "702" "B" Nothing (Lam "705" False "707" "x" Nothing (App (AppTp (App (Var "712" "SigmaInd") False (Var "721" "x")) (TpParens "725" (TpLam "726" "728" "x" (Tkt (TpApp (TpApp (TpVar "732" "Sigma") (TpVar "740" "A")) (TpVar "744" "B"))) (TpVar "747" "A")) "749")) False (Parens "750" (Lam "751" False "753" "a" Nothing (Lam "756" False "758" "b" Nothing (Var "761" "a"))) "763")))))) "764",CmdDef Nothing (DefTerm "766" "snd" (Just (TpAbs "772" True "774" "A" (Tkk (KdStar "778")) (TpAbs "781" True "783" "B" (Tkk (KdArrow (Tkt (TpVar "787" "A")) (KdStar "791"))) (TpAbs "794" False "796" "x" (Tkt (TpApp (TpApp (TpVar "800" "Sigma") (TpVar "808" "A")) (TpVar "812" "B"))) (TpAppt (TpVar "815" "B") (Parens "817" (App (Var "818" "fst") False (Var "822" "x")) "824")))))) (Lam "827" True "829" "A" Nothing (Lam "832" True "834" "B" Nothing (Lam "837" False "839" "x" Nothing (App (AppTp (App (Var "844" "SigmaInd") False (Var "853" "x")) (TpParens "857" (TpLam "858" "860" "x" (Tkt (TpApp (TpApp (TpVar "864" "Sigma") (TpVar "872" "A")) (TpVar "876" "B"))) (TpAppt (TpVar "879" "B") (Parens "881" (App (Var "882" "fst") False (Var "886" "x")) "888"))) "889")) False (Parens "890" (Lam "891" False "893" "a" Nothing (Lam "896" False "898" "b" Nothing (Var "901" "b"))) "903")))))) "904",CmdDef Nothing (DefType "907" "Cast" (KdArrow (Tkk (KdParens "914" (KdArrow (Tkt (TpVar "915" "Indices")) (KdStar "925")) "927")) (KdArrow (Tkk (KdParens "930" (KdArrow (Tkt (TpVar "931" "Indices")) (KdStar "941")) "943")) (KdStar "946"))) (TpLam "950" "952" "A" (Tkk (KdArrow (Tkt (TpVar "956" "Indices")) (KdStar "966"))) (TpLam "969" "971" "B" (Tkk (KdArrow (Tkt (TpVar "975" "Indices")) (KdStar "985"))) (TpIota "990" "992" "cast" (TpAbs "999" True "1001" "indices" (Tkt (TpVar "1011" "Indices")) (TpArrow (TpAppt (TpVar "1020" "A") (Var "1022" "indices")) False (TpAppt (TpVar "1032" "B") (Var "1034" "indices")))) (TpEq "1043" (Var "1044" "cast") (Lam "1051" False "1053" "x" Nothing (Var "1056" "x")) "1058"))))) "1059",CmdDef Nothing (DefTerm "1061" "cast" (Just (TpAbs "1072" True "1074" "A" (Tkk (KdArrow (Tkt (TpVar "1078" "Indices")) (KdStar "1088"))) (TpAbs "1091" True "1093" "B" (Tkk (KdArrow (Tkt (TpVar "1097" "Indices")) (KdStar "1107"))) (TpArrow (TpApp (TpApp (TpVar "1110" "Cast") (TpVar "1117" "A")) (TpVar "1121" "B")) True (TpAbs "1129" True "1131" "indices" (Tkt (TpVar "1141" "Indices")) (TpArrow (TpAppt (TpVar "1150" "A") (Var "1152" "indices")) False (TpAppt (TpVar "1162" "B") (Var "1164" "indices")))))))) (Lam "1176" True "1178" "A" Nothing (Lam "1181" True "1183" "B" Nothing (Lam "1186" True "1188" "c" Nothing (Phi "1191" (IotaProj (Var "1193" "c") "2" "1196") (IotaProj (Var "1199" "c") "1" "1202") (Lam "1204" False "1206" "x" Nothing (Var "1209" "x")) "1211"))))) "1212",CmdDef Nothing (DefType "1214" "Functor" (KdArrow (Tkk (KdParens "1224" (KdArrow (Tkk (KdParens "1225" (KdArrow (Tkt (TpVar "1226" "Indices")) (KdStar "1236")) "1238")) (KdArrow (Tkt (TpVar "1241" "Indices")) (KdStar "1251"))) "1253")) (KdStar "1256")) (TpLam "1262" "1264" "F" (Tkk (KdArrow (Tkk (KdParens "1268" (KdArrow (Tkt (TpVar "1269" "Indices")) (KdStar "1279")) "1281")) (KdArrow (Tkt (TpVar "1284" "Indices")) (KdStar "1294")))) (TpAbs "1297" True "1299" "X" (Tkk (KdArrow (Tkt (TpVar "1303" "Indices")) (KdStar "1313"))) (TpAbs "1316" True "1318" "Y" (Tkk (KdArrow (Tkt (TpVar "1322" "Indices")) (KdStar "1332"))) (TpArrow (TpApp (TpApp (TpVar "1339" "Cast") (TpVar "1346" "X")) (TpVar "1350" "Y")) True (TpApp (TpApp (TpVar "1354" "Cast") (TpParens "1361" (TpApp (TpVar "1362" "F") (TpVar "1366" "X")) "1368")) (TpParens "1371" (TpApp (TpVar "1372" "F") (TpVar "1376" "Y")) "1378"))))))) "1379",CmdDef Nothing (DefType "1382" "AlgM" (KdArrow (Tkk (KdParens "1389" (KdArrow (Tkk (KdParens "1390" (KdArrow (Tkt (TpVar "1391" "Indices")) (KdStar "1401")) "1403")) (KdArrow (Tkt (TpVar "1406" "Indices")) (KdStar "1416"))) "1418")) (KdArrow (Tkk (KdStar "1421")) (KdArrow (Tkt (TpVar "1425" "Indices")) (KdStar "1435")))) (TpLam "1441" "1443" "F" (Tkk (KdArrow (Tkk (KdParens "1447" (KdArrow (Tkt (TpVar "1448" "Indices")) (KdStar "1458")) "1460")) (KdArrow (Tkt (TpVar "1463" "Indices")) (KdStar "1473")))) (TpLam "1476" "1478" "A" (Tkk (KdStar "1482")) (TpLam "1485" "1487" "indices" (Tkt (TpVar "1497" "Indices")) (TpAbs "1510" True "1512" "R" (Tkk (KdArrow (Tkt (TpVar "1516" "Indices")) (KdStar "1526"))) (TpArrow (TpParens "1529" (TpArrow (TpAppt (TpVar "1530" "R") (Var "1532" "indices")) False (TpVar "1542" "A")) "1544") False (TpArrow (TpAppt (TpApp (TpVar "1547" "F") (TpVar "1551" "R")) (Var "1553" "indices")) False (TpVar "1563" "A")))))))) "1565",CmdDef Nothing (DefType "1567" "FixM" (KdArrow (Tkk (KdParens "1574" (KdArrow (Tkk (KdParens "1575" (KdArrow (Tkt (TpVar "1576" "Indices")) (KdStar "1586")) "1588")) (KdArrow (Tkt (TpVar "1591" "Indices")) (KdStar "1601"))) "1603")) (KdArrow (Tkt (TpVar "1606" "Indices")) (KdStar "1616"))) (TpLam "1622" "1624" "F" (Tkk (KdArrow (Tkk (KdParens "1628" (KdArrow (Tkt (TpVar "1629" "Indices")) (KdStar "1639")) "1641")) (KdArrow (Tkt (TpVar "1644" "Indices")) (KdStar "1654")))) (TpLam "1657" "1659" "indices" (Tkt (TpVar "1669" "Indices")) (TpAbs "1678" True "1680" "A" (Tkk (KdStar "1684")) (TpArrow (TpAppt (TpApp (TpApp (TpVar "1687" "AlgM") (TpVar "1694" "F")) (TpVar "1698" "A")) (Var "1700" "indices")) False (TpVar "1710" "A")))))) "1712",CmdDef Nothing (DefTerm "1714" "foldM" (Just (TpAbs "1726" True "1728" "F" (Tkk (KdArrow (Tkk (KdParens "1732" (KdArrow (Tkt (TpVar "1733" "Indices")) (KdStar "1743")) "1745")) (KdArrow (Tkt (TpVar "1748" "Indices")) (KdStar "1758")))) (TpAbs "1761" True "1763" "A" (Tkk (KdStar "1767")) (TpAbs "1770" True "1772" "indices" (Tkt (TpVar "1782" "Indices")) (TpArrow (TpAppt (TpApp (TpApp (TpVar "1795" "AlgM") (TpVar "1802" "F")) (TpVar "1806" "A")) (Var "1808" "indices")) False (TpArrow (TpAppt (TpApp (TpVar "1818" "FixM") (TpVar "1825" "F")) (Var "1827" "indices")) False (TpVar "1837" "A"))))))) (Lam "1843" True "1845" "F" Nothing (Lam "1848" True "1850" "A" Nothing (Lam "1853" True "1855" "indices" Nothing (Lam "1864" False "1866" "alg" Nothing (Lam "1871" False "1873" "fix" Nothing (App (Var "1878" "fix") False (Var "1882" "alg")))))))) "1886",CmdDef Nothing (DefTerm "1888" "inFixM" (Just (TpAbs "1901" True "1903" "F" (Tkk (KdArrow (Tkk (KdParens "1907" (KdArrow (Tkt (TpVar "1908" "Indices")) (KdStar "1918")) "1920")) (KdArrow (Tkt (TpVar "1923" "Indices")) (KdStar "1933")))) (TpAbs "1936" True "1938" "indices" (Tkt (TpVar "1948" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "1961" "F") (TpParens "1965" (TpApp (TpVar "1966" "FixM") (TpVar "1973" "F")) "1975")) (Var "1976" "indices")) False (TpAppt (TpApp (TpVar "1986" "FixM") (TpVar "1993" "F")) (Var "1995" "indices")))))) (Lam "2007" True "2009" "F" Nothing (Lam "2012" True "2014" "indices" Nothing (Lam "2023" False "2025" "fexp" Nothing (Lam "2031" True "2033" "A" Nothing (Lam "2036" False "2038" "alg" Nothing (App (App (Var "2043" "alg") False (Parens "2047" (App (App (AppTp (AppTp (Var "2048" "foldM") (TpVar "2056" "F")) (TpVar "2060" "A")) True (Var "2063" "indices")) False (Var "2071" "alg")) "2075")) False (Var "2076" "fexp")))))))) "2081",CmdDef Nothing (DefType "2083" "PrfAlgM" (KdAbs "2097" "2099" "F" (Tkk (KdArrow (Tkk (KdParens "2103" (KdArrow (Tkt (TpVar "2104" "Indices")) (KdStar "2114")) "2116")) (KdArrow (Tkt (TpVar "2119" "Indices")) (KdStar "2129")))) (KdArrow (Tkt (TpApp (TpVar "2136" "Functor") (TpVar "2146" "F"))) (KdAbs "2154" "2156" "X" (Tkk (KdArrow (Tkt (TpVar "2160" "Indices")) (KdStar "2170"))) (KdArrow (Tkk (KdParens "2177" (KdAbs "2178" "2180" "indices" (Tkt (TpVar "2190" "Indices")) (KdArrow (Tkt (TpAppt (TpVar "2199" "X") (Var "2201" "indices"))) (KdStar "2211"))) "2213")) (KdArrow (Tkt (TpParens "2220" (TpAbs "2221" True "2223" "indices" (Tkt (TpVar "2233" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "2242" "F") (TpVar "2246" "X")) (Var "2248" "indices")) False (TpAppt (TpVar "2258" "X") (Var "2260" "indices")))) "2268")) (KdStar "2275")))))) (TpLam "2281" "2283" "F" (Tkk (KdArrow (Tkk (KdParens "2287" (KdArrow (Tkt (TpVar "2288" "Indices")) (KdStar "2298")) "2300")) (KdArrow (Tkt (TpVar "2303" "Indices")) (KdStar "2313")))) (TpLam "2316" "2318" "fmap" (Tkt (TpApp (TpVar "2325" "Functor") (TpVar "2335" "F"))) (TpLam "2338" "2340" "X" (Tkk (KdArrow (Tkt (TpVar "2344" "Indices")) (KdStar "2354"))) (TpLam "2361" "2363" "Q" (Tkk (KdAbs "2367" "2369" "indices" (Tkt (TpVar "2379" "Indices")) (KdArrow (Tkt (TpAppt (TpVar "2388" "X") (Var "2390" "indices"))) (KdStar "2400")))) (TpLam "2409" "2411" "alg" (Tkt (TpParens "2417" (TpAbs "2418" True "2420" "indices" (Tkt (TpVar "2430" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "2439" "F") (TpVar "2443" "X")) (Var "2445" "indices")) False (TpAppt (TpVar "2455" "X") (Var "2457" "indices")))) "2465")) (TpAbs "2476" True "2478" "R" (Tkk (KdArrow (Tkt (TpVar "2482" "Indices")) (KdStar "2492"))) (TpAbs "2495" True "2497" "c" (Tkt (TpApp (TpApp (TpVar "2501" "Cast") (TpVar "2508" "R")) (TpVar "2512" "X"))) (TpArrow (TpParens "2524" (TpAbs "2525" True "2527" "indices" (Tkt (TpVar "2537" "Indices")) (TpAbs "2546" False "2548" "r" (Tkt (TpAppt (TpVar "2552" "R") (Var "2554" "indices"))) (TpAppt (TpAppt (TpVar "2563" "Q") (Var "2565" "indices")) (Parens "2573" (App (App (App (Var "2574" "cast") True (Var "2580" "c")) True (Var "2583" "indices")) False (Var "2591" "r")) "2593")))) "2594") False (TpAbs "2605" True "2607" "indices" (Tkt (TpVar "2617" "Indices")) (TpAbs "2626" False "2628" "gr" (Tkt (TpAppt (TpApp (TpVar "2633" "F") (TpVar "2637" "R")) (Var "2639" "indices"))) (TpAppt (TpAppt (TpVar "2656" "Q") (Var "2658" "indices")) (Parens "2666" (App (App (Var "2667" "alg") True (Var "2672" "indices")) False (Parens "2680" (App (App (App (Var "2681" "cast") True (Parens "2687" (App (Var "2688" "fmap") True (Var "2694" "c")) "2696")) True (Var "2698" "indices")) False (Var "2706" "gr")) "2709")) "2710"))))))))))))) "2711",CmdDef Nothing (DefType "2713" "IsIndFixM" (KdAbs "2729" "2731" "F" (Tkk (KdArrow (Tkk (KdParens "2735" (KdArrow (Tkt (TpVar "2736" "Indices")) (KdStar "2746")) "2748")) (KdArrow (Tkt (TpVar "2751" "Indices")) (KdStar "2761")))) (KdArrow (Tkt (TpApp (TpVar "2768" "Functor") (TpVar "2778" "F"))) (KdAbs "2786" "2788" "indices" (Tkt (TpVar "2798" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpVar "2811" "FixM") (TpVar "2818" "F")) (Var "2820" "indices"))) (KdStar "2834"))))) (TpLam "2840" "2842" "F" (Tkk (KdArrow (Tkk (KdParens "2846" (KdArrow (Tkt (TpVar "2847" "Indices")) (KdStar "2857")) "2859")) (KdArrow (Tkt (TpVar "2862" "Indices")) (KdStar "2872")))) (TpLam "2875" "2877" "fmap" (Tkt (TpApp (TpVar "2884" "Functor") (TpVar "2894" "F"))) (TpLam "2901" "2903" "indices" (Tkt (TpVar "2913" "Indices")) (TpLam "2922" "2924" "x" (Tkt (TpAppt (TpApp (TpVar "2928" "FixM") (TpVar "2935" "F")) (Var "2937" "indices"))) (TpAbs "2952" True "2954" "Q" (Tkk (KdAbs "2958" "2960" "indices" (Tkt (TpVar "2970" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpVar "2979" "FixM") (TpVar "2986" "F")) (Var "2988" "indices"))) (KdStar "2998")))) (TpArrow (TpAppt (TpApp (TpApp (TpAppt (TpApp (TpVar "3007" "PrfAlgM") (TpVar "3017" "F")) (Var "3019" "fmap")) (TpParens "3026" (TpApp (TpVar "3027" "FixM") (TpVar "3034" "F")) "3036")) (TpVar "3039" "Q")) (Parens "3041" (AppTp (Var "3042" "inFixM") (TpVar "3051" "F")) "3053")) False (TpAppt (TpAppt (TpVar "3056" "Q") (Var "3058" "indices")) (Var "3066" "x"))))))))) "3068",CmdDef Nothing (DefType "3070" "FixIndM" (KdAbs "3080" "3082" "F" (Tkk (KdArrow (Tkk (KdParens "3086" (KdArrow (Tkt (TpVar "3087" "Indices")) (KdStar "3097")) "3099")) (KdArrow (Tkt (TpVar "3102" "Indices")) (KdStar "3112")))) (KdArrow (Tkt (TpApp (TpVar "3115" "Functor") (TpVar "3125" "F"))) (KdArrow (Tkt (TpVar "3129" "Indices")) (KdStar "3139")))) (TpLam "3145" "3147" "F" (Tkk (KdArrow (Tkk (KdParens "3151" (KdArrow (Tkt (TpVar "3152" "Indices")) (KdStar "3162")) "3164")) (KdArrow (Tkt (TpVar "3167" "Indices")) (KdStar "3177")))) (TpLam "3180" "3182" "fmap" (Tkt (TpApp (TpVar "3189" "Functor") (TpVar "3199" "F"))) (TpLam "3202" "3204" "indices" (Tkt (TpVar "3214" "Indices")) (TpIota "3227" "3229" "x" (TpAppt (TpApp (TpVar "3233" "FixM") (TpVar "3240" "F")) (Var "3242" "indices")) (TpAppt (TpAppt (TpAppt (TpApp (TpVar "3251" "IsIndFixM") (TpVar "3263" "F")) (Var "3265" "fmap")) (Var "3270" "indices")) (Var "3278" "x"))))))) "3280",CmdDef Nothing (DefTerm "3282" "inFixIndM" (Just (TpAbs "3294" True "3296" "F" (Tkk (KdArrow (Tkk (KdParens "3300" (KdArrow (Tkt (TpVar "3301" "Indices")) (KdStar "3311")) "3313")) (KdArrow (Tkt (TpVar "3316" "Indices")) (KdStar "3326")))) (TpAbs "3329" True "3331" "fmap" (Tkt (TpApp (TpVar "3338" "Functor") (TpVar "3348" "F"))) (TpAbs "3355" True "3357" "indices" (Tkt (TpVar "3367" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "3376" "F") (TpParens "3380" (TpAppt (TpApp (TpVar "3381" "FixIndM") (TpVar "3391" "F")) (Var "3393" "fmap")) "3398")) (Var "3399" "indices")) False (TpAppt (TpAppt (TpApp (TpVar "3409" "FixIndM") (TpVar "3419" "F")) (Var "3421" "fmap")) (Var "3426" "indices"))))))) (Lam "3438" True "3440" "F" Nothing (Lam "3443" True "3445" "fmap" Nothing (Lam "3451" True "3453" "indices" Nothing (Lam "3462" False "3464" "v" Nothing (Let "3471" False (DefTerm "3472" "outInd" (Just (TpApp (TpApp (TpVar "3481" "Cast") (TpParens "3488" (TpAppt (TpApp (TpVar "3489" "FixIndM") (TpVar "3499" "F")) (Var "3501" "fmap")) "3506")) (TpParens "3509" (TpApp (TpVar "3510" "FixM") (TpVar "3517" "F")) "3519"))) (IotaPair "3522" (Lam "3523" True "3525" "indices" Nothing (Lam "3534" False "3536" "x" Nothing (IotaProj (Var "3539" "x") "1" "3542"))) (Beta "3544" Nothing Nothing) Nothing "3546")) (IotaPair "3554" (App (App (AppTp (Var "3555" "inFixM") (TpVar "3564" "F")) True (Var "3567" "indices")) False (Parens "3575" (App (App (App (Var "3576" "cast") True (Parens "3582" (App (Var "3583" "fmap") True (Var "3589" "outInd")) "3596")) True (Var "3598" "indices")) False (Var "3606" "v")) "3608")) (Lam "3615" True "3617" "Q" Nothing (Lam "3620" False "3622" "q" Nothing (App (App (App (App (Var "3625" "q") True (Var "3628" "outInd")) False (Parens "3635" (Lam "3636" True "3638" "indices" Nothing (Lam "3647" False "3649" "r" Nothing (App (IotaProj (Var "3652" "r") "2" "3655") False (Var "3656" "q")))) "3658")) True (Var "3660" "indices")) False (Var "3668" "v")))) Nothing "3671"))))))) "3672",CmdDef Nothing (DefType "3674" "WithWitness" (KdAbs "3688" "3690" "X" (Tkk (KdStar "3694")) (KdAbs "3697" "3699" "Y" (Tkk (KdStar "3703")) (KdArrow (Tkk (KdParens "3706" (KdArrow (Tkt (TpVar "3707" "X")) (KdStar "3711")) "3713")) (KdArrow (Tkt (TpVar "3716" "Y")) (KdStar "3720"))))) (TpLam "3726" "3728" "X" (Tkk (KdStar "3732")) (TpLam "3735" "3737" "Y" (Tkk (KdStar "3741")) (TpLam "3744" "3746" "Q" (Tkk (KdArrow (Tkt (TpVar "3750" "X")) (KdStar "3754"))) (TpLam "3757" "3759" "y" (Tkt (TpVar "3763" "Y")) (TpApp (TpApp (TpVar "3770" "Sigma") (TpParens "3778" (TpIota "3779" "3781" "x" (TpVar "3785" "X") (TpEq "3788" (Var "3789" "y") (Var "3793" "x") "3795")) "3796")) (TpParens "3799" (TpLam "3800" "3802" "x" (Tkt (TpParens "3806" (TpIota "3807" "3809" "x" (TpVar "3813" "X") (TpEq "3816" (Var "3817" "y") (Var "3821" "x") "3823")) "3824")) (TpAppt (TpVar "3826" "Q") (IotaProj (Var "3828" "x") "1" "3831"))) "3832"))))))) "3833",CmdDef Nothing (DefType "3835" "Lift" (KdAbs "3846" "3848" "F" (Tkk (KdArrow (Tkk (KdParens "3852" (KdArrow (Tkt (TpVar "3853" "Indices")) (KdStar "3863")) "3865")) (KdArrow (Tkt (TpVar "3868" "Indices")) (KdStar "3878")))) (KdAbs "3881" "3883" "fmap" (Tkt (TpApp (TpVar "3890" "Functor") (TpVar "3900" "F"))) (KdArrow (Tkk (KdParens "3907" (KdAbs "3908" "3910" "indices" (Tkt (TpVar "3920" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "3929" "FixIndM") (TpVar "3939" "F")) (Var "3941" "fmap")) (Var "3946" "indices"))) (KdStar "3956"))) "3958")) (KdAbs "3965" "3967" "indices" (Tkt (TpVar "3977" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpVar "3986" "FixM") (TpVar "3993" "F")) (Var "3995" "indices"))) (KdStar "4009")))))) (TpLam "4015" "4017" "F" (Tkk (KdArrow (Tkk (KdParens "4021" (KdArrow (Tkt (TpVar "4022" "Indices")) (KdStar "4032")) "4034")) (KdArrow (Tkt (TpVar "4037" "Indices")) (KdStar "4047")))) (TpLam "4050" "4052" "fmap" (Tkt (TpApp (TpVar "4059" "Functor") (TpVar "4069" "F"))) (TpLam "4076" "4078" "Q" (Tkk (KdAbs "4082" "4084" "indices" (Tkt (TpVar "4094" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "4103" "FixIndM") (TpVar "4113" "F")) (Var "4115" "fmap")) (Var "4120" "indices"))) (KdStar "4130")))) (TpLam "4139" "4141" "indices" (Tkt (TpVar "4151" "Indices")) (TpLam "4160" "4162" "e" (Tkt (TpAppt (TpApp (TpVar "4166" "FixM") (TpVar "4173" "F")) (Var "4175" "indices"))) (TpAppt (TpApp (TpApp (TpApp (TpVar "4192" "WithWitness") (TpParens "4206" (TpAppt (TpAppt (TpApp (TpVar "4207" "FixIndM") (TpVar "4217" "F")) (Var "4219" "fmap")) (Var "4224" "indices")) "4232")) (TpParens "4235" (TpAppt (TpApp (TpVar "4236" "FixM") (TpVar "4243" "F")) (Var "4245" "indices")) "4253")) (TpParens "4256" (TpAppt (TpVar "4257" "Q") (Var "4259" "indices")) "4267")) (Var "4268" "e")))))))) "4270",CmdDef Nothing (DefTerm "4272" "LiftProp1" (Just (TpAbs "4288" True "4290" "F" (Tkk (KdArrow (Tkk (KdParens "4294" (KdArrow (Tkt (TpVar "4295" "Indices")) (KdStar "4305")) "4307")) (KdArrow (Tkt (TpVar "4310" "Indices")) (KdStar "4320")))) (TpAbs "4323" True "4325" "fmap" (Tkt (TpApp (TpVar "4332" "Functor") (TpVar "4342" "F"))) (TpAbs "4349" True "4351" "Q" (Tkk (KdAbs "4355" "4357" "indices" (Tkt (TpVar "4367" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "4376" "FixIndM") (TpVar "4386" "F")) (Var "4388" "fmap")) (Var "4393" "indices"))) (KdStar "4403")))) (TpAbs "4410" True "4412" "indices" (Tkt (TpVar "4422" "Indices")) (TpAbs "4431" True "4433" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "4437" "FixIndM") (TpVar "4447" "F")) (Var "4449" "fmap")) (Var "4454" "indices"))) (TpArrow (TpAppt (TpAppt (TpApp (TpAppt (TpApp (TpVar "4467" "Lift") (TpVar "4474" "F")) (Var "4476" "fmap")) (TpVar "4483" "Q")) (Var "4485" "indices")) (IotaProj (Var "4493" "e") "1" "4496")) False (TpAppt (TpAppt (TpVar "4499" "Q") (Var "4501" "indices")) (Var "4509" "e"))))))))) (Lam "4515" True "4517" "F" Nothing (Lam "4520" True "4522" "fmap" Nothing (Lam "4528" True "4530" "Q" Nothing (Lam "4533" True "4535" "indices" Nothing (Lam "4544" True "4546" "e" Nothing (Lam "4549" False "4551" "pr" Nothing (Rho "4555" False Nothing (IotaProj (Parens "4557" (App (Var "4558" "fst") False (Var "4562" "pr")) "4565") "2" "4567") Nothing (App (Var "4570" "snd") False (Var "4574" "pr")))))))))) "4577",CmdDef Nothing (DefTerm "4579" "LiftProp2" (Just (TpAbs "4595" True "4597" "F" (Tkk (KdArrow (Tkk (KdParens "4601" (KdArrow (Tkt (TpVar "4602" "Indices")) (KdStar "4612")) "4614")) (KdArrow (Tkt (TpVar "4617" "Indices")) (KdStar "4627")))) (TpAbs "4630" True "4632" "fmap" (Tkt (TpApp (TpVar "4639" "Functor") (TpVar "4649" "F"))) (TpAbs "4656" True "4658" "Q" (Tkk (KdAbs "4662" "4664" "indices" (Tkt (TpVar "4674" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "4683" "FixIndM") (TpVar "4693" "F")) (Var "4695" "fmap")) (Var "4700" "indices"))) (KdStar "4710")))) (TpAbs "4717" True "4719" "indices" (Tkt (TpVar "4729" "Indices")) (TpAbs "4738" False "4740" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "4744" "FixIndM") (TpVar "4754" "F")) (Var "4756" "fmap")) (Var "4761" "indices"))) (TpArrow (TpAppt (TpAppt (TpVar "4774" "Q") (Var "4776" "indices")) (Var "4784" "e")) False (TpAppt (TpAppt (TpApp (TpAppt (TpApp (TpVar "4788" "Lift") (TpVar "4795" "F")) (Var "4797" "fmap")) (TpVar "4804" "Q")) (Var "4806" "indices")) (IotaProj (Var "4814" "e") "1" "4817"))))))))) (Lam "4822" True "4824" "F" Nothing (Lam "4827" True "4829" "fmap" Nothing (Lam "4835" True "4837" "Q" Nothing (Lam "4840" True "4842" "indices" Nothing (Lam "4851" False "4853" "e" Nothing (App (AppTp (AppTp (Var "4856" "sigma") (TpParens "4868" (TpIota "4869" "4871" "x" (TpAppt (TpAppt (TpApp (TpVar "4875" "FixIndM") (TpVar "4885" "F")) (Var "4887" "fmap")) (Var "4892" "indices")) (TpEq "4901" (Var "4902" "e") (Var "4906" "x") "4908")) "4909")) (TpParens "4916" (TpLam "4917" "4919" "x" (Tkt (TpIota "4923" "4925" "x" (TpAppt (TpAppt (TpApp (TpVar "4929" "FixIndM") (TpVar "4939" "F")) (Var "4941" "fmap")) (Var "4946" "indices")) (TpEq "4955" (Var "4956" "e") (Var "4960" "x") "4962"))) (TpAppt (TpAppt (TpVar "4964" "Q") (Var "4966" "indices")) (IotaProj (Var "4974" "x") "1" "4977"))) "4978")) False (IotaPair "4983" (Var "4984" "e") (Beta "4987" Nothing (Just (PosTerm (Var "4989" "e") "4991"))) Nothing "4992")))))))) "4993",CmdDef Nothing (DefTerm "4995" "LiftProp3" (Just (TpAbs "5011" True "5013" "F" (Tkk (KdArrow (Tkk (KdParens "5017" (KdArrow (Tkt (TpVar "5018" "Indices")) (KdStar "5028")) "5030")) (KdArrow (Tkt (TpVar "5033" "Indices")) (KdStar "5043")))) (TpAbs "5046" True "5048" "fmap" (Tkt (TpApp (TpVar "5055" "Functor") (TpVar "5065" "F"))) (TpAbs "5072" True "5074" "Q" (Tkk (KdAbs "5078" "5080" "indices" (Tkt (TpVar "5090" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "5099" "FixIndM") (TpVar "5109" "F")) (Var "5111" "fmap")) (Var "5116" "indices"))) (KdStar "5126")))) (TpAbs "5133" True "5135" "indices" (Tkt (TpVar "5145" "Indices")) (TpAbs "5154" True "5156" "e" (Tkt (TpAppt (TpApp (TpVar "5160" "FixM") (TpVar "5167" "F")) (Var "5169" "indices"))) (TpArrow (TpAppt (TpAppt (TpApp (TpAppt (TpApp (TpVar "5182" "Lift") (TpVar "5189" "F")) (Var "5191" "fmap")) (TpVar "5198" "Q")) (Var "5200" "indices")) (Var "5208" "e")) False (TpAppt (TpAppt (TpApp (TpVar "5212" "FixIndM") (TpVar "5222" "F")) (Var "5224" "fmap")) (Var "5229" "indices"))))))))) (Lam "5241" True "5243" "F" Nothing (Lam "5246" True "5248" "fmap" Nothing (Lam "5254" True "5256" "Q" Nothing (Lam "5259" True "5261" "indices" Nothing (Lam "5270" True "5272" "e" Nothing (Lam "5275" False "5277" "pr" Nothing (IotaProj (Parens "5281" (App (Var "5282" "fst") False (Var "5286" "pr")) "5289") "1" "5291")))))))) "5292",CmdDef Nothing (DefTerm "5294" "LiftProp4" (Just (TpAbs "5310" True "5312" "F" (Tkk (KdArrow (Tkk (KdParens "5316" (KdArrow (Tkt (TpVar "5317" "Indices")) (KdStar "5327")) "5329")) (KdArrow (Tkt (TpVar "5332" "Indices")) (KdStar "5342")))) (TpAbs "5345" True "5347" "fmap" (Tkt (TpApp (TpVar "5354" "Functor") (TpVar "5364" "F"))) (TpAbs "5371" True "5373" "Q" (Tkk (KdAbs "5377" "5379" "indices" (Tkt (TpVar "5389" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "5398" "FixIndM") (TpVar "5408" "F")) (Var "5410" "fmap")) (Var "5415" "indices"))) (KdStar "5425")))) (TpAbs "5432" True "5434" "indices" (Tkt (TpVar "5444" "Indices")) (TpAbs "5453" True "5455" "e" (Tkt (TpAppt (TpApp (TpVar "5459" "FixM") (TpVar "5466" "F")) (Var "5468" "indices"))) (TpAbs "5481" True "5483" "p" (Tkt (TpAppt (TpAppt (TpApp (TpAppt (TpApp (TpVar "5487" "Lift") (TpVar "5494" "F")) (Var "5496" "fmap")) (TpVar "5503" "Q")) (Var "5505" "indices")) (Var "5513" "e"))) (TpEq "5516" (App (Var "5517" "LiftProp3") False (Var "5527" "p")) (Var "5531" "e") "5533")))))))) (Lam "5538" True "5540" "F" Nothing (Lam "5543" True "5545" "fmap" Nothing (Lam "5551" True "5553" "Q" Nothing (Lam "5556" True "5558" "indices" Nothing (Lam "5567" True "5569" "e" Nothing (Lam "5572" True "5574" "pr" Nothing (Rho "5578" False Nothing (IotaProj (Parens "5580" (App (Var "5581" "fst") False (Var "5585" "pr")) "5588") "2" "5590") Nothing (Beta "5593" Nothing Nothing))))))))) "5595",CmdDef Nothing (DefTerm "5597" "convIH" (Just (TpAbs "5607" True "5609" "F" (Tkk (KdArrow (Tkk (KdParens "5613" (KdArrow (Tkt (TpVar "5614" "Indices")) (KdStar "5624")) "5626")) (KdArrow (Tkt (TpVar "5629" "Indices")) (KdStar "5639")))) (TpAbs "5642" True "5644" "fmap" (Tkt (TpApp (TpVar "5651" "Functor") (TpVar "5661" "F"))) (TpAbs "5665" True "5667" "Q" (Tkk (KdAbs "5671" "5673" "indices" (Tkt (TpVar "5683" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "5692" "FixIndM") (TpVar "5702" "F")) (Var "5704" "fmap")) (Var "5709" "indices"))) (KdStar "5719")))) (TpAbs "5723" True "5725" "Y" (Tkk (KdAbs "5729" "5731" "indices" (Tkt (TpVar "5741" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpVar "5750" "FixM") (TpVar "5757" "F")) (Var "5759" "indices"))) (KdStar "5769")))) (TpAbs "5773" False "5775" "Yprop1" (Tkt (TpAbs "5784" True "5786" "indices" (Tkt (TpVar "5796" "Indices")) (TpAbs "5805" True "5807" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "5811" "FixIndM") (TpVar "5821" "F")) (Var "5823" "fmap")) (Var "5828" "indices"))) (TpArrow (TpAppt (TpAppt (TpVar "5837" "Y") (Var "5839" "indices")) (IotaProj (Var "5847" "e") "1" "5850")) False (TpAppt (TpAppt (TpVar "5853" "Q") (Var "5855" "indices")) (Var "5863" "e")))))) (TpAbs "5867" False "5869" "Yprop2" (Tkt (TpAbs "5878" True "5880" "indices" (Tkt (TpVar "5890" "Indices")) (TpAbs "5899" False "5901" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "5905" "FixIndM") (TpVar "5915" "F")) (Var "5917" "fmap")) (Var "5922" "indices"))) (TpArrow (TpAppt (TpAppt (TpVar "5931" "Q") (Var "5933" "indices")) (Var "5941" "e")) False (TpAppt (TpAppt (TpVar "5945" "Y") (Var "5947" "indices")) (IotaProj (Var "5955" "e") "1" "5958")))))) (TpAbs "5961" False "5963" "Yprop3" (Tkt (TpAbs "5972" True "5974" "indices" (Tkt (TpVar "5984" "Indices")) (TpAbs "5993" True "5995" "e" (Tkt (TpAppt (TpApp (TpVar "5999" "FixM") (TpVar "6006" "F")) (Var "6008" "indices"))) (TpArrow (TpAppt (TpAppt (TpVar "6017" "Y") (Var "6019" "indices")) (Var "6027" "e")) False (TpAppt (TpAppt (TpApp (TpVar "6031" "FixIndM") (TpVar "6041" "F")) (Var "6043" "fmap")) (Var "6048" "indices")))))) (TpAbs "6058" False "6060" "Yprop4" (Tkt (TpAbs "6069" True "6071" "indices" (Tkt (TpVar "6081" "Indices")) (TpAbs "6090" True "6092" "e" (Tkt (TpAppt (TpApp (TpVar "6096" "FixM") (TpVar "6103" "F")) (Var "6105" "indices"))) (TpAbs "6114" True "6116" "p" (Tkt (TpAppt (TpAppt (TpVar "6120" "Y") (Var "6122" "indices")) (Var "6130" "e"))) (TpEq "6133" (App (Var "6134" "Yprop3") False (Var "6141" "p")) (Var "6145" "e") "6147"))))) (TpArrow (TpAppt (TpApp (TpApp (TpAppt (TpApp (TpVar "6150" "PrfAlgM") (TpVar "6160" "F")) (Var "6162" "fmap")) (TpParens "6169" (TpAppt (TpApp (TpVar "6170" "FixIndM") (TpVar "6180" "F")) (Var "6182" "fmap")) "6187")) (TpVar "6190" "Q")) (Parens "6192" (App (AppTp (Var "6193" "inFixIndM") (TpVar "6205" "F")) True (Var "6208" "fmap")) "6213")) False (TpAppt (TpApp (TpApp (TpAppt (TpApp (TpVar "6217" "PrfAlgM") (TpVar "6227" "F")) (Var "6229" "fmap")) (TpParens "6236" (TpApp (TpVar "6237" "FixM") (TpVar "6244" "F")) "6246")) (TpVar "6249" "Y")) (Parens "6251" (AppTp (Var "6252" "inFixM") (TpVar "6261" "F")) "6263")))))))))))) (Lam "6268" True "6270" "F" Nothing (Lam "6273" True "6275" "fmap" Nothing (Lam "6281" True "6283" "Q" Nothing (Lam "6286" True "6288" "Y" Nothing (Lam "6291" False "6293" "qp3" Nothing (Lam "6298" False "6300" "qp4" Nothing (Lam "6305" False "6307" "qp1" Nothing (Lam "6312" False "6314" "qp2" Nothing (Lam "6319" False "6321" "q" Nothing (Lam "6324" True "6326" "R" Nothing (Lam "6329" True "6331" "cst" Nothing (Lam "6336" False "6338" "ih" Nothing (Lam "6342" True "6344" "indices" Nothing (Lam "6353" False "6355" "gr" Nothing (Let "6363" False (DefTerm "6364" "cst2" (Just (TpApp (TpApp (TpVar "6371" "Cast") (TpVar "6378" "R")) (TpParens "6382" (TpAppt (TpApp (TpVar "6383" "FixIndM") (TpVar "6393" "F")) (Var "6395" "fmap")) "6400"))) (IotaPair "6409" (Lam "6410" True "6412" "indices" Nothing (Lam "6421" False "6423" "r" Nothing (Phi "6426" (Parens "6428" (App (App (App (Var "6429" "qp2") True (Var "6434" "indices")) True (Parens "6443" (App (App (App (Var "6444" "cast") True (Var "6450" "cst")) True (Var "6455" "indices")) False (Var "6463" "r")) "6465")) True (Parens "6467" (App (App (Var "6468" "ih") True (Var "6472" "indices")) False (Var "6480" "r")) "6482")) "6483") (Parens "6494" (App (App (App (Var "6495" "qp1") True (Var "6500" "indices")) True (Parens "6509" (App (App (App (Var "6510" "cast") True (Var "6516" "cst")) True (Var "6521" "indices")) False (Var "6529" "r")) "6531")) False (Parens "6532" (App (App (Var "6533" "ih") True (Var "6537" "indices")) False (Var "6545" "r")) "6547")) "6548") (Var "6550" "r") "6552"))) (Beta "6554" Nothing Nothing) Nothing "6556")) (App (App (App (Var "6564" "qp4") True (Var "6569" "indices")) False (Parens "6577" (App (App (App (Var "6578" "inFixIndM") True (Var "6589" "fmap")) True (Var "6595" "indices")) False (Parens "6603" (App (App (App (Var "6604" "cast") True (Parens "6610" (App (Var "6611" "fmap") True (Var "6617" "cst2")) "6622")) True (Var "6624" "indices")) False (Var "6632" "gr")) "6635")) "6636")) False (Parens "6643" (App (App (App (App (Var "6644" "q") True (Var "6647" "cst2")) False (Parens "6652" (Lam "6653" True "6655" "indices" Nothing (Lam "6664" False "6666" "r" Nothing (App (App (App (Var "6669" "qp3") True (Var "6674" "indices")) True (Parens "6683" (App (App (App (Var "6684" "cast") True (Var "6690" "cst2")) True (Var "6696" "indices")) False (Var "6704" "r")) "6706")) False (Parens "6707" (App (App (Var "6708" "ih") True (Var "6712" "indices")) False (Var "6720" "r")) "6722")))) "6723")) True (Var "6733" "indices")) False (Var "6741" "gr")) "6744")))))))))))))))))) "6745",CmdDef Nothing (DefTerm "6747" "indFixIndM" (Just (TpAbs "6760" True "6762" "F" (Tkk (KdArrow (Tkk (KdParens "6766" (KdArrow (Tkt (TpVar "6767" "Indices")) (KdStar "6777")) "6779")) (KdArrow (Tkt (TpVar "6782" "Indices")) (KdStar "6792")))) (TpAbs "6795" True "6797" "fmap" (Tkt (TpApp (TpVar "6804" "Functor") (TpVar "6814" "F"))) (TpAbs "6830" True "6832" "indices" (Tkt (TpVar "6842" "Indices")) (TpAbs "6851" False "6853" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "6857" "FixIndM") (TpVar "6867" "F")) (Var "6869" "fmap")) (Var "6874" "indices"))) (TpAbs "6896" True "6898" "Q" (Tkk (KdAbs "6902" "6904" "indices" (Tkt (TpVar "6914" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "6923" "FixIndM") (TpVar "6933" "F")) (Var "6935" "fmap")) (Var "6940" "indices"))) (KdStar "6950")))) (TpArrow (TpAppt (TpApp (TpApp (TpAppt (TpApp (TpVar "6966" "PrfAlgM") (TpVar "6976" "F")) (Var "6978" "fmap")) (TpParens "6985" (TpAppt (TpApp (TpVar "6986" "FixIndM") (TpVar "6996" "F")) (Var "6998" "fmap")) "7003")) (TpVar "7006" "Q")) (Parens "7008" (App (AppTp (Var "7009" "inFixIndM") (TpVar "7021" "F")) True (Var "7024" "fmap")) "7029")) False (TpAppt (TpAppt (TpVar "7045" "Q") (Var "7047" "indices")) (Var "7055" "e"))))))))) (Lam "7062" True "7064" "F" Nothing (Lam "7067" True "7069" "fmap" Nothing (Lam "7075" True "7077" "indices" Nothing (Lam "7086" False "7088" "e" Nothing (Lam "7091" True "7093" "Q" Nothing (Lam "7096" False "7098" "q" Nothing (App (App (App (AppTp (App (Var "7101" "LiftProp1") True (Var "7112" "fmap")) (TpVar "7119" "Q")) True (Var "7122" "indices")) True (Var "7131" "e")) False (Parens "7137" (App (IotaProj (Var "7138" "e") "2" "7141") False (Parens "7142" (App (App (App (App (App (App (Var "7143" "convIH") True (Var "7151" "fmap")) False (Parens "7162" (AppTp (App (Var "7163" "LiftProp1") True (Var "7174" "fmap")) (TpVar "7181" "Q")) "7183")) False (Parens "7190" (AppTp (App (Var "7191" "LiftProp2") True (Var "7202" "fmap")) (TpVar "7209" "Q")) "7211")) False (Parens "7218" (AppTp (App (Var "7219" "LiftProp3") True (Var "7230" "fmap")) (TpVar "7237" "Q")) "7239")) False (Parens "7246" (AppTp (App (Var "7247" "LiftProp4") True (Var "7258" "fmap")) (TpVar "7265" "Q")) "7267")) False (Var "7274" "q")) "7276")) "7277"))))))))) "7278",CmdDef Nothing (DefTerm "7281" "outAlgM" (Just (TpAbs "7295" True "7297" "F" (Tkk (KdArrow (Tkk (KdParens "7301" (KdArrow (Tkt (TpVar "7302" "Indices")) (KdStar "7312")) "7314")) (KdArrow (Tkt (TpVar "7317" "Indices")) (KdStar "7327")))) (TpAbs "7330" True "7332" "fmap" (Tkt (TpApp (TpVar "7339" "Functor") (TpVar "7349" "F"))) (TpAppt (TpApp (TpApp (TpAppt (TpApp (TpVar "7352" "PrfAlgM") (TpVar "7362" "F")) (Var "7364" "fmap")) (TpParens "7377" (TpAppt (TpApp (TpVar "7378" "FixIndM") (TpVar "7388" "F")) (Var "7390" "fmap")) "7395")) (TpParens "7398" (TpLam "7399" "7401" "indices" (Tkt (TpVar "7411" "Indices")) (TpLam "7420" "7422" "_" (Tkt (TpAppt (TpAppt (TpApp (TpVar "7426" "FixIndM") (TpVar "7436" "F")) (Var "7438" "fmap")) (Var "7443" "indices"))) (TpAppt (TpApp (TpVar "7483" "F") (TpParens "7487" (TpAppt (TpApp (TpVar "7488" "FixIndM") (TpVar "7498" "F")) (Var "7500" "fmap")) "7505")) (Var "7506" "indices")))) "7514")) (Parens "7515" (App (AppTp (Var "7516" "inFixIndM") (TpVar "7528" "F")) True (Var "7531" "fmap")) "7536"))))) (Lam "7541" True "7543" "F" Nothing (Lam "7546" True "7548" "fmap" Nothing (Lam "7554" True "7556" "R" Nothing (Lam "7559" True "7561" "c" Nothing (Lam "7564" False "7566" "x" Nothing (App (Var "7569" "cast") True (Parens "7575" (App (Var "7576" "fmap") True (Var "7582" "c")) "7584")))))))) "7585",CmdDef Nothing (DefTerm "7587" "outFixIndM" (Just (TpAbs "7604" True "7606" "F" (Tkk (KdArrow (Tkk (KdParens "7610" (KdArrow (Tkt (TpVar "7611" "Indices")) (KdStar "7621")) "7623")) (KdArrow (Tkt (TpVar "7626" "Indices")) (KdStar "7636")))) (TpAbs "7639" True "7641" "fmap" (Tkt (TpApp (TpVar "7648" "Functor") (TpVar "7658" "F"))) (TpAbs "7661" True "7663" "indices" (Tkt (TpVar "7673" "Indices")) (TpArrow (TpAppt (TpAppt (TpApp (TpVar "7686" "FixIndM") (TpVar "7696" "F")) (Var "7698" "fmap")) (Var "7703" "indices")) False (TpAppt (TpApp (TpVar "7713" "F") (TpParens "7717" (TpAppt (TpApp (TpVar "7718" "FixIndM") (TpVar "7728" "F")) (Var "7730" "fmap")) "7735")) (Var "7736" "indices"))))))) (Lam "7748" True "7750" "F" Nothing (Lam "7753" True "7755" "fmap" Nothing (Lam "7761" True "7763" "indices" Nothing (Lam "7772" False "7774" "e" Nothing (App (AppTp (App (App (App (Var "7777" "indFixIndM") True (Var "7789" "fmap")) True (Var "7795" "indices")) False (Var "7803" "e")) (TpParens "7811" (TpLam "7812" "7814" "indices" (Tkt (TpVar "7824" "Indices")) (TpLam "7833" "7835" "_" (Tkt (TpAppt (TpAppt (TpApp (TpVar "7839" "FixIndM") (TpVar "7849" "F")) (Var "7851" "fmap")) (Var "7856" "indices"))) (TpAppt (TpApp (TpVar "7865" "F") (TpParens "7869" (TpAppt (TpApp (TpVar "7870" "FixIndM") (TpVar "7880" "F")) (Var "7882" "fmap")) "7887")) (Var "7888" "indices")))) "7896")) False (Parens "7901" (App (AppTp (Var "7902" "outAlgM") (TpVar "7912" "F")) True (Var "7915" "fmap")) "7920"))))))) "7921",CmdDef Nothing (DefType "7924" "Cowedge" (KdArrow (Tkk (KdParens "7934" (KdArrow (Tkk (KdParens "7935" (KdArrow (Tkt (TpVar "7936" "Indices")) (KdStar "7946")) "7948")) (KdArrow (Tkt (TpVar "7951" "Indices")) (KdStar "7961"))) "7963")) (KdArrow (Tkk (KdParens "7966" (KdArrow (Tkt (TpVar "7967" "Indices")) (KdStar "7977")) "7979")) (KdArrow (Tkt (TpVar "7982" "Indices")) (KdStar "7992")))) (TpLam "7998" "8000" "F" (Tkk (KdArrow (Tkk (KdParens "8004" (KdArrow (Tkt (TpVar "8005" "Indices")) (KdStar "8015")) "8017")) (KdArrow (Tkt (TpVar "8020" "Indices")) (KdStar "8030")))) (TpLam "8033" "8035" "D" (Tkk (KdArrow (Tkt (TpVar "8039" "Indices")) (KdStar "8049"))) (TpLam "8052" "8054" "indices" (Tkt (TpVar "8064" "Indices")) (TpAbs "8077" True "8079" "A" (Tkk (KdArrow (Tkt (TpVar "8083" "Indices")) (KdStar "8093"))) (TpArrow (TpParens "8100" (TpAbs "8101" True "8103" "indices" (Tkt (TpVar "8113" "Indices")) (TpArrow (TpAppt (TpVar "8122" "A") (Var "8124" "indices")) False (TpAppt (TpVar "8134" "D") (Var "8136" "indices")))) "8144") False (TpArrow (TpAppt (TpApp (TpVar "8151" "F") (TpVar "8155" "A")) (Var "8157" "indices")) False (TpAppt (TpVar "8171" "D") (Var "8173" "indices"))))))))) "8181",CmdDef Nothing (DefType "8182" "Coend" (KdArrow (Tkk (KdParens "8190" (KdArrow (Tkk (KdParens "8191" (KdArrow (Tkt (TpVar "8192" "Indices")) (KdStar "8202")) "8204")) (KdArrow (Tkt (TpVar "8207" "Indices")) (KdStar "8217"))) "8219")) (KdArrow (Tkk (KdParens "8222" (KdArrow (Tkt (TpVar "8223" "Indices")) (KdStar "8233")) "8235")) (KdArrow (Tkt (TpVar "8238" "Indices")) (KdStar "8248")))) (TpLam "8254" "8256" "F" (Tkk (KdArrow (Tkk (KdParens "8260" (KdArrow (Tkt (TpVar "8261" "Indices")) (KdStar "8271")) "8273")) (KdArrow (Tkt (TpVar "8276" "Indices")) (KdStar "8286")))) (TpLam "8289" "8291" "A" (Tkk (KdArrow (Tkt (TpVar "8295" "Indices")) (KdStar "8305"))) (TpLam "8308" "8310" "indices" (Tkt (TpVar "8320" "Indices")) (TpAbs "8333" True "8335" "Y" (Tkk (KdStar "8339")) (TpArrow (TpParens "8346" (TpAbs "8347" True "8349" "R" (Tkk (KdArrow (Tkt (TpVar "8353" "Indices")) (KdStar "8363"))) (TpArrow (TpParens "8366" (TpAbs "8367" True "8369" "indices" (Tkt (TpVar "8379" "Indices")) (TpArrow (TpAppt (TpVar "8388" "R") (Var "8390" "indices")) False (TpAppt (TpVar "8400" "A") (Var "8402" "indices")))) "8410") False (TpArrow (TpAppt (TpApp (TpVar "8413" "F") (TpVar "8417" "R")) (Var "8419" "indices")) False (TpVar "8429" "Y")))) "8431") False (TpVar "8438" "Y"))))))) "8440",CmdDef Nothing (DefTerm "8442" "intrCoend" (Just (TpAbs "8458" True "8460" "F" (Tkk (KdArrow (Tkk (KdParens "8464" (KdArrow (Tkt (TpVar "8465" "Indices")) (KdStar "8475")) "8477")) (KdArrow (Tkt (TpVar "8480" "Indices")) (KdStar "8490")))) (TpAbs "8497" True "8499" "C" (Tkk (KdArrow (Tkt (TpVar "8503" "Indices")) (KdStar "8513"))) (TpAbs "8520" True "8522" "R" (Tkk (KdArrow (Tkt (TpVar "8526" "Indices")) (KdStar "8536"))) (TpAbs "8543" True "8545" "indices" (Tkt (TpVar "8555" "Indices")) (TpArrow (TpParens "8568" (TpAbs "8569" True "8571" "indices" (Tkt (TpVar "8581" "Indices")) (TpArrow (TpAppt (TpVar "8590" "R") (Var "8592" "indices")) False (TpAppt (TpVar "8602" "C") (Var "8604" "indices")))) "8612") False (TpArrow (TpAppt (TpApp (TpVar "8619" "F") (TpVar "8623" "R")) (Var "8625" "indices")) False (TpAppt (TpApp (TpApp (TpVar "8639" "Coend") (TpVar "8647" "F")) (TpVar "8651" "C")) (Var "8653" "indices"))))))))) (Lam "8665" True "8667" "F" Nothing (Lam "8670" True "8672" "C" Nothing (Lam "8675" True "8677" "R" Nothing (Lam "8680" True "8682" "indices" Nothing (Lam "8691" False "8693" "ac" Nothing (Lam "8697" False "8699" "ga" Nothing (Lam "8703" True "8705" "Y" Nothing (Lam "8708" False "8710" "q" Nothing (App (App (Var "8713" "q") False (Var "8715" "ac")) False (Var "8718" "ga"))))))))))) "8721",CmdDef Nothing (DefTerm "8723" "elimCoend" (Just (TpAbs "8739" True "8741" "F" (Tkk (KdArrow (Tkk (KdParens "8745" (KdArrow (Tkt (TpVar "8746" "Indices")) (KdStar "8756")) "8758")) (KdArrow (Tkt (TpVar "8761" "Indices")) (KdStar "8771")))) (TpAbs "8778" True "8780" "A" (Tkk (KdArrow (Tkt (TpVar "8784" "Indices")) (KdStar "8794"))) (TpAbs "8801" True "8803" "D" (Tkk (KdStar "8807")) (TpAbs "8814" True "8816" "indices" (Tkt (TpVar "8826" "Indices")) (TpArrow (TpParens "8839" (TpAbs "8840" True "8842" "R" (Tkk (KdArrow (Tkt (TpVar "8846" "Indices")) (KdStar "8856"))) (TpArrow (TpParens "8859" (TpAbs "8860" True "8862" "indices" (Tkt (TpVar "8872" "Indices")) (TpArrow (TpAppt (TpVar "8881" "R") (Var "8883" "indices")) False (TpAppt (TpVar "8893" "A") (Var "8895" "indices")))) "8903") False (TpArrow (TpAppt (TpApp (TpVar "8906" "F") (TpVar "8910" "R")) (Var "8912" "indices")) False (TpVar "8922" "D")))) "8924") False (TpArrow (TpAppt (TpApp (TpApp (TpVar "8931" "Coend") (TpVar "8939" "F")) (TpVar "8943" "A")) (Var "8945" "indices")) False (TpVar "8959" "D")))))))) (Lam "8965" True "8967" "F" Nothing (Lam "8970" True "8972" "A" Nothing (Lam "8975" True "8977" "D" Nothing (Lam "8980" True "8982" "indices" Nothing (Lam "8991" False "8993" "phi" Nothing (Lam "8998" False "9000" "e" Nothing (App (Var "9003" "e") False (Var "9005" "phi"))))))))) "9009",CmdDef Nothing (DefType "9011" "CoendInductive" (KdAbs "9032" "9034" "F" (Tkk (KdArrow (Tkk (KdParens "9038" (KdArrow (Tkt (TpVar "9039" "Indices")) (KdStar "9049")) "9051")) (KdArrow (Tkt (TpVar "9054" "Indices")) (KdStar "9064")))) (KdAbs "9067" "9069" "C" (Tkk (KdArrow (Tkt (TpVar "9073" "Indices")) (KdStar "9083"))) (KdAbs "9090" "9092" "indices" (Tkt (TpVar "9102" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpApp (TpVar "9111" "Coend") (TpVar "9119" "F")) (TpVar "9123" "C")) (Var "9125" "indices"))) (KdStar "9135"))))) (TpLam "9141" "9143" "F" (Tkk (KdArrow (Tkk (KdParens "9147" (KdArrow (Tkt (TpVar "9148" "Indices")) (KdStar "9158")) "9160")) (KdArrow (Tkt (TpVar "9163" "Indices")) (KdStar "9173")))) (TpLam "9176" "9178" "C" (Tkk (KdArrow (Tkt (TpVar "9182" "Indices")) (KdStar "9192"))) (TpLam "9199" "9201" "indices" (Tkt (TpVar "9211" "Indices")) (TpLam "9220" "9222" "e" (Tkt (TpAppt (TpApp (TpApp (TpVar "9226" "Coend") (TpVar "9234" "F")) (TpVar "9238" "C")) (Var "9240" "indices"))) (TpAbs "9255" True "9257" "Q" (Tkk (KdAbs "9261" "9263" "indices" (Tkt (TpVar "9273" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpApp (TpVar "9282" "Coend") (TpVar "9290" "F")) (TpVar "9294" "C")) (Var "9296" "indices"))) (KdStar "9306")))) (TpArrow (TpParens "9315" (TpAbs "9316" True "9318" "R" (Tkk (KdArrow (Tkt (TpVar "9322" "Indices")) (KdStar "9332"))) (TpAbs "9335" True "9337" "indices" (Tkt (TpVar "9347" "Indices")) (TpAbs "9356" False "9358" "c" (Tkt (TpApp (TpApp (TpVar "9362" "Cast") (TpVar "9369" "R")) (TpVar "9373" "C"))) (TpAbs "9384" False "9386" "gr" (Tkt (TpAppt (TpApp (TpVar "9391" "F") (TpVar "9395" "R")) (Var "9397" "indices"))) (TpAppt (TpAppt (TpVar "9406" "Q") (Var "9408" "indices")) (Parens "9416" (App (App (App (AppTp (AppTp (AppTp (Var "9417" "intrCoend") (TpVar "9429" "F")) (TpVar "9433" "C")) (TpVar "9437" "R")) True (Var "9440" "indices")) False (Parens "9448" (App (Var "9449" "cast") True (Var "9455" "c")) "9457")) False (Var "9458" "gr")) "9461")))))) "9462") False (TpAppt (TpAppt (TpVar "9471" "Q") (Var "9473" "indices")) (Var "9481" "e"))))))))) "9483",CmdDef Nothing (DefType "9485" "CoendInd" (KdArrow (Tkk (KdParens "9496" (KdArrow (Tkk (KdParens "9497" (KdArrow (Tkt (TpVar "9498" "Indices")) (KdStar "9508")) "9510")) (KdArrow (Tkt (TpVar "9513" "Indices")) (KdStar "9523"))) "9525")) (KdArrow (Tkk (KdParens "9528" (KdArrow (Tkt (TpVar "9529" "Indices")) (KdStar "9539")) "9541")) (KdArrow (Tkt (TpVar "9544" "Indices")) (KdStar "9554")))) (TpLam "9560" "9562" "G" (Tkk (KdArrow (Tkk (KdParens "9566" (KdArrow (Tkt (TpVar "9567" "Indices")) (KdStar "9577")) "9579")) (KdArrow (Tkt (TpVar "9582" "Indices")) (KdStar "9592")))) (TpLam "9595" "9597" "C" (Tkk (KdArrow (Tkt (TpVar "9601" "Indices")) (KdStar "9611"))) (TpLam "9614" "9616" "indices" (Tkt (TpVar "9626" "Indices")) (TpIota "9639" "9641" "x" (TpAppt (TpApp (TpApp (TpVar "9645" "Coend") (TpVar "9653" "G")) (TpVar "9657" "C")) (Var "9659" "indices")) (TpAppt (TpAppt (TpApp (TpApp (TpVar "9668" "CoendInductive") (TpVar "9686" "G")) (TpVar "9690" "C")) (Var "9692" "indices")) (Var "9700" "x"))))))) "9702",CmdDef Nothing (DefTerm "9705" "intrCoendInd" (Just (TpAbs "9724" True "9726" "F" (Tkk (KdArrow (Tkk (KdParens "9730" (KdArrow (Tkt (TpVar "9731" "Indices")) (KdStar "9741")) "9743")) (KdArrow (Tkt (TpVar "9746" "Indices")) (KdStar "9756")))) (TpAbs "9763" True "9765" "C" (Tkk (KdArrow (Tkt (TpVar "9769" "Indices")) (KdStar "9779"))) (TpAbs "9782" True "9784" "R" (Tkk (KdArrow (Tkt (TpVar "9788" "Indices")) (KdStar "9798"))) (TpAbs "9801" True "9803" "indices" (Tkt (TpVar "9813" "Indices")) (TpArrow (TpApp (TpApp (TpVar "9826" "Cast") (TpVar "9833" "R")) (TpVar "9837" "C")) True (TpArrow (TpAppt (TpApp (TpVar "9841" "F") (TpVar "9845" "R")) (Var "9847" "indices")) False (TpAppt (TpApp (TpApp (TpVar "9857" "CoendInd") (TpVar "9868" "F")) (TpVar "9872" "C")) (Var "9874" "indices"))))))))) (Lam "9886" True "9888" "F" Nothing (Lam "9891" True "9893" "C" Nothing (Lam "9896" True "9898" "R" Nothing (Lam "9901" True "9903" "indices" Nothing (Lam "9912" True "9914" "f" Nothing (Lam "9917" False "9919" "gr" Nothing (IotaPair "9927" (App (App (App (AppTp (AppTp (AppTp (Var "9928" "intrCoend") (TpVar "9940" "F")) (TpVar "9944" "C")) (TpVar "9948" "R")) True (Var "9951" "indices")) False (Parens "9959" (App (Var "9960" "cast") True (Var "9966" "f")) "9968")) False (Var "9969" "gr")) (Lam "9973" True "9975" "Q" Nothing (Lam "9978" False "9980" "q" Nothing (App (App (App (AppTp (Var "9983" "q") (TpVar "9987" "R")) True (Var "9990" "indices")) False (IotaPair "9998" (App (Var "9999" "cast") True (Var "10005" "f")) (Beta "10008" Nothing Nothing) Nothing "10010")) False (Var "10011" "gr")))) Nothing "10014")))))))) "10015",CmdDef Nothing (DefTerm "10018" "indCoend'" (Just (TpAbs "10034" True "10036" "F" (Tkk (KdArrow (Tkk (KdParens "10040" (KdArrow (Tkt (TpVar "10041" "Indices")) (KdStar "10051")) "10053")) (KdArrow (Tkt (TpVar "10056" "Indices")) (KdStar "10066")))) (TpAbs "10069" True "10071" "C" (Tkk (KdArrow (Tkt (TpVar "10075" "Indices")) (KdStar "10085"))) (TpAbs "10088" True "10090" "indices" (Tkt (TpVar "10100" "Indices")) (TpAbs "10113" False "10115" "e" (Tkt (TpAppt (TpApp (TpApp (TpVar "10119" "CoendInd") (TpVar "10130" "F")) (TpVar "10134" "C")) (Var "10136" "indices"))) (TpAbs "10149" True "10151" "Q" (Tkk (KdAbs "10155" "10157" "indices" (Tkt (TpVar "10167" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpApp (TpVar "10176" "CoendInd") (TpVar "10187" "F")) (TpVar "10191" "C")) (Var "10193" "indices"))) (KdStar "10203")))) (TpArrow (TpParens "10210" (TpAbs "10211" True "10213" "R" (Tkk (KdArrow (Tkt (TpVar "10217" "Indices")) (KdStar "10227"))) (TpAbs "10230" True "10232" "indices" (Tkt (TpVar "10242" "Indices")) (TpAbs "10251" True "10253" "c" (Tkt (TpApp (TpApp (TpVar "10257" "Cast") (TpVar "10264" "R")) (TpVar "10268" "C"))) (TpAbs "10277" False "10279" "gr" (Tkt (TpAppt (TpApp (TpVar "10284" "F") (TpVar "10288" "R")) (Var "10290" "indices"))) (TpAppt (TpAppt (TpVar "10299" "Q") (Var "10301" "indices")) (Parens "10309" (App (App (App (AppTp (AppTp (AppTp (Var "10310" "intrCoendInd") (TpVar "10325" "F")) (TpVar "10329" "C")) (TpVar "10333" "R")) True (Var "10336" "indices")) True (Var "10345" "c")) False (Var "10347" "gr")) "10350")))))) "10351") False (TpAbs "10358" True "10360" "X" (Tkk (KdAbs "10364" "10366" "indices" (Tkt (TpVar "10376" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpApp (TpVar "10385" "CoendInd") (TpVar "10396" "F")) (TpVar "10400" "C")) (Var "10402" "indices"))) (KdStar "10412")))) (TpArrow (TpParens "10419" (TpAbs "10420" True "10422" "indices" (Tkt (TpVar "10432" "Indices")) (TpAbs "10441" True "10443" "x'" (Tkt (TpAppt (TpApp (TpApp (TpVar "10448" "CoendInd") (TpVar "10459" "F")) (TpVar "10463" "C")) (Var "10465" "indices"))) (TpArrow (TpAppt (TpAppt (TpVar "10474" "Q") (Var "10476" "indices")) (Var "10484" "x'")) False (TpAppt (TpAppt (TpVar "10489" "X") (Var "10491" "indices")) (Var "10499" "x'"))))) "10502") False (TpAppt (TpAppt (TpVar "10509" "X") (Var "10511" "indices")) (Var "10519" "e"))))))))))) (Lam "10525" True "10527" "F" Nothing (Lam "10530" True "10532" "C" Nothing (Lam "10535" True "10537" "indices" Nothing (Lam "10546" False "10548" "e" Nothing (Lam "10551" True "10553" "Q" Nothing (Lam "10556" False "10558" "q" Nothing (App (App (App (AppTp (IotaProj (Var "10561" "e") "2" "10564") (TpParens "10567" (TpLam "10568" "10570" "indices" (Tkt (TpVar "10580" "Indices")) (TpLam "10589" "10591" "e" (Tkt (TpAppt (TpApp (TpApp (TpVar "10595" "Coend") (TpVar "10603" "F")) (TpVar "10607" "C")) (Var "10609" "indices"))) (TpAbs "10618" True "10620" "e'" (Tkt (TpAppt (TpApp (TpApp (TpVar "10625" "CoendInd") (TpVar "10636" "F")) (TpVar "10640" "C")) (Var "10642" "indices"))) (TpAbs "10651" True "10653" "eq" (Tkt (TpEq "10658" (Var "10659" "e'") (Var "10664" "e") "10666")) (TpAbs "10668" True "10670" "X" (Tkk (KdAbs "10674" "10676" "indices'" (Tkt (TpVar "10687" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpApp (TpVar "10697" "CoendInd") (TpVar "10708" "F")) (TpVar "10712" "C")) (Var "10714" "indices'"))) (KdStar "10725")))) (TpArrow (TpParens "10729" (TpAbs "10730" True "10732" "indices'" (Tkt (TpVar "10743" "Indices")) (TpAbs "10753" True "10755" "x'" (Tkt (TpAppt (TpApp (TpApp (TpVar "10760" "CoendInd") (TpVar "10771" "F")) (TpVar "10775" "C")) (Var "10777" "indices'"))) (TpArrow (TpAppt (TpAppt (TpVar "10788" "Q") (Var "10790" "indices'")) (Var "10799" "x'")) False (TpAppt (TpAppt (TpVar "10804" "X") (Var "10806" "indices'")) (Var "10815" "x'"))))) "10818") False (TpAppt (TpAppt (TpVar "10821" "X") (Var "10823" "indices")) (Parens "10831" (Phi "10832" (Var "10834" "eq") (Var "10839" "e'") (Var "10843" "e") "10845") "10846")))))))) "10847")) False (Parens "10852" (Lam "10853" True "10855" "R" Nothing (Lam "10858" True "10860" "indices" Nothing (Lam "10869" False "10871" "ar" Nothing (Lam "10875" False "10877" "gr" Nothing (Lam "10881" True "10883" "e'" Nothing (Lam "10887" True "10889" "eq" Nothing (Lam "10893" True "10895" "X" Nothing (Lam "10898" False "10900" "qq" Nothing (App (App (App (Var "10904" "qq") True (Var "10908" "indices")) True (Parens "10923" (App (App (App (AppTp (AppTp (AppTp (Var "10924" "intrCoendInd") (TpVar "10939" "F")) (TpVar "10943" "C")) (TpVar "10947" "R")) True (Var "10950" "indices")) True (Var "10959" "ar")) False (Var "10962" "gr")) "10965")) False (Parens "10966" (App (App (App (AppTp (Var "10967" "q") (TpVar "10971" "R")) True (Var "10974" "indices")) True (Var "10983" "ar")) False (Var "10986" "gr")) "10989")))))))))) "10990")) True (Var "10992" "e")) True (Beta "10995" Nothing Nothing))))))))) "10997",CmdDef Nothing (DefTerm "11000" "indCoend" (Just (TpAbs "11015" True "11017" "F" (Tkk (KdArrow (Tkk (KdParens "11021" (KdArrow (Tkt (TpVar "11022" "Indices")) (KdStar "11032")) "11034")) (KdArrow (Tkt (TpVar "11037" "Indices")) (KdStar "11047")))) (TpAbs "11050" True "11052" "C" (Tkk (KdArrow (Tkt (TpVar "11056" "Indices")) (KdStar "11066"))) (TpAbs "11069" True "11071" "indices" (Tkt (TpVar "11081" "Indices")) (TpAbs "11094" False "11096" "e" (Tkt (TpAppt (TpApp (TpApp (TpVar "11100" "CoendInd") (TpVar "11111" "F")) (TpVar "11115" "C")) (Var "11117" "indices"))) (TpAbs "11130" True "11132" "Q" (Tkk (KdAbs "11136" "11138" "indices" (Tkt (TpVar "11148" "Indices")) (KdArrow (Tkt (TpAppt (TpApp (TpApp (TpVar "11157" "CoendInd") (TpVar "11168" "F")) (TpVar "11172" "C")) (Var "11174" "indices"))) (KdStar "11184")))) (TpArrow (TpParens "11191" (TpAbs "11192" True "11194" "R" (Tkk (KdArrow (Tkt (TpVar "11198" "Indices")) (KdStar "11208"))) (TpAbs "11211" True "11213" "indices" (Tkt (TpVar "11223" "Indices")) (TpAbs "11232" True "11234" "c" (Tkt (TpApp (TpApp (TpVar "11238" "Cast") (TpVar "11245" "R")) (TpVar "11249" "C"))) (TpAbs "11258" False "11260" "gr" (Tkt (TpAppt (TpApp (TpVar "11265" "F") (TpVar "11269" "R")) (Var "11271" "indices"))) (TpAppt (TpAppt (TpVar "11280" "Q") (Var "11282" "indices")) (Parens "11290" (App (App (App (AppTp (AppTp (AppTp (Var "11291" "intrCoendInd") (TpVar "11306" "F")) (TpVar "11310" "C")) (TpVar "11314" "R")) True (Var "11317" "indices")) True (Var "11326" "c")) False (Var "11328" "gr")) "11331")))))) "11332") False (TpAppt (TpAppt (TpVar "11339" "Q") (Var "11341" "indices")) (Var "11349" "e"))))))))) (Lam "11355" True "11357" "F" Nothing (Lam "11360" True "11362" "C" Nothing (Lam "11365" True "11367" "indices" Nothing (Lam "11376" False "11378" "e" Nothing (Lam "11381" True "11383" "Q" Nothing (Lam "11386" False "11388" "i" Nothing (App (AppTp (App (AppTp (App (App (AppTp (AppTp (Var "11395" "indCoend'") (TpVar "11407" "F")) (TpVar "11411" "C")) True (Var "11414" "indices")) False (Var "11422" "e")) (TpVar "11426" "Q")) False (Var "11428" "i")) (TpVar "11432" "Q")) False (Parens "11434" (Lam "11435" True "11437" "indices" Nothing (Lam "11446" True "11448" "x'" Nothing (Lam "11452" False "11454" "u" Nothing (Var "11457" "u")))) "11459"))))))))) "11460",CmdDef Nothing (DefTerm "11462" "fmapCoend" (Just (TpAbs "11474" True "11476" "F" (Tkk (KdArrow (Tkk (KdParens "11480" (KdArrow (Tkt (TpVar "11481" "Indices")) (KdStar "11491")) "11493")) (KdArrow (Tkt (TpVar "11496" "Indices")) (KdStar "11506")))) (TpApp (TpVar "11509" "Functor") (TpParens "11519" (TpApp (TpVar "11520" "CoendInd") (TpVar "11531" "F")) "11533")))) (Lam "11538" True "11540" "F" Nothing (Lam "11543" True "11545" "A" Nothing (Lam "11548" True "11550" "B" Nothing (Lam "11553" True "11555" "f" Nothing (IotaPair "11562" (Lam "11563" True "11565" "indices" Nothing (Lam "11574" False "11576" "c" Nothing (Phi "11585" (Parens "11587" (Theta "11588" (AbstractVars ["indices","c"]) (Parens "11601" (App (App (AppTp (AppTp (Var "11602" "indCoend") (TpVar "11613" "F")) (TpVar "11617" "A")) True (Var "11620" "indices")) False (Var "11628" "c")) "11630") [Lterm False (Parens "11631" (Lam "11632" True "11634" "R" Nothing (Lam "11637" True "11639" "indices" Nothing (Lam "11648" True "11650" "i" Nothing (Lam "11653" False "11655" "gr" Nothing (Beta "11659" Nothing Nothing))))) "11661")]) "11662") (Theta "11674" (AbstractVars ["indices","c"]) (Parens "11687" (App (App (AppTp (AppTp (Var "11688" "indCoend") (TpVar "11699" "F")) (TpVar "11703" "A")) True (Var "11706" "indices")) False (Var "11714" "c")) "11716") [Lterm False (Parens "11717" (Lam "11718" True "11720" "R" Nothing (Lam "11723" True "11725" "indices" Nothing (Lam "11734" True "11736" "i" Nothing (Lam "11739" False "11741" "gr" Nothing (App (App (App (AppTp (AppTp (AppTp (Var "11756" "intrCoendInd") (TpVar "11771" "F")) (TpVar "11775" "B")) (TpVar "11779" "R")) True (Var "11782" "indices")) True (IotaPair "11804" (Lam "11805" True "11807" "indices" Nothing (Lam "11816" False "11818" "r" Nothing (App (App (App (Var "11821" "cast") True (Var "11827" "f")) True (Var "11830" "indices")) False (Parens "11838" (App (App (App (Var "11839" "cast") True (Var "11845" "i")) True (Var "11848" "indices")) False (Var "11856" "r")) "11858")))) (Beta "11860" Nothing Nothing) Nothing "11862")) False (Var "11863" "gr")))))) "11866")]) (Var "11868" "c") "11870"))) (Beta "11872" Nothing Nothing) Nothing "11874")))))) "11875",CmdDef Nothing (DefType "11878" "AlgCVM" (KdArrow (Tkk (KdParens "11887" (KdArrow (Tkk (KdParens "11888" (KdArrow (Tkt (TpVar "11889" "Indices")) (KdStar "11899")) "11901")) (KdArrow (Tkt (TpVar "11904" "Indices")) (KdStar "11914"))) "11916")) (KdArrow (Tkk (KdStar "11919")) (KdArrow (Tkt (TpVar "11923" "Indices")) (KdStar "11933")))) (TpLam "11939" "11941" "F" (Tkk (KdArrow (Tkk (KdParens "11945" (KdArrow (Tkt (TpVar "11946" "Indices")) (KdStar "11956")) "11958")) (KdArrow (Tkt (TpVar "11961" "Indices")) (KdStar "11971")))) (TpLam "11974" "11976" "X" (Tkk (KdStar "11980")) (TpLam "11983" "11985" "indices" (Tkt (TpVar "11995" "Indices")) (TpAbs "12008" True "12010" "R" (Tkk (KdArrow (Tkt (TpVar "12014" "Indices")) (KdStar "12024"))) (TpArrow (TpParens "12027" (TpArrow (TpAppt (TpVar "12028" "R") (Var "12030" "indices")) False (TpAppt (TpApp (TpVar "12040" "F") (TpVar "12044" "R")) (Var "12046" "indices"))) "12054") False (TpArrow (TpParens "12057" (TpArrow (TpAppt (TpVar "12058" "R") (Var "12060" "indices")) False (TpVar "12070" "X")) "12072") False (TpArrow (TpAppt (TpApp (TpVar "12075" "F") (TpVar "12079" "R")) (Var "12081" "indices")) False (TpVar "12091" "X"))))))))) "12093",CmdDef Nothing (DefType "12096" "FixCVM" (KdArrow (Tkk (KdParens "12105" (KdArrow (Tkk (KdParens "12106" (KdArrow (Tkt (TpVar "12107" "Indices")) (KdStar "12117")) "12119")) (KdArrow (Tkt (TpVar "12122" "Indices")) (KdStar "12132"))) "12134")) (KdArrow (Tkt (TpVar "12137" "Indices")) (KdStar "12147"))) (TpLam "12153" "12155" "F" (Tkk (KdArrow (Tkk (KdParens "12159" (KdArrow (Tkt (TpVar "12160" "Indices")) (KdStar "12170")) "12172")) (KdArrow (Tkt (TpVar "12175" "Indices")) (KdStar "12185")))) (TpLam "12188" "12190" "indices" (Tkt (TpVar "12200" "Indices")) (TpAbs "12213" True "12215" "R" (Tkk (KdStar "12219")) (TpArrow (TpAppt (TpApp (TpApp (TpVar "12222" "AlgCVM") (TpVar "12231" "F")) (TpVar "12235" "R")) (Var "12237" "indices")) False (TpVar "12247" "R")))))) "12249",CmdDef Nothing (DefTerm "12251" "foldCVM" (Just (TpAbs "12265" True "12267" "F" (Tkk (KdArrow (Tkk (KdParens "12271" (KdArrow (Tkt (TpVar "12272" "Indices")) (KdStar "12282")) "12284")) (KdArrow (Tkt (TpVar "12287" "Indices")) (KdStar "12297")))) (TpAbs "12300" True "12302" "A" (Tkk (KdStar "12306")) (TpAbs "12309" True "12311" "indices" (Tkt (TpVar "12321" "Indices")) (TpArrow (TpAppt (TpApp (TpApp (TpVar "12334" "AlgCVM") (TpVar "12343" "F")) (TpVar "12347" "A")) (Var "12349" "indices")) False (TpArrow (TpAppt (TpApp (TpVar "12359" "FixCVM") (TpVar "12368" "F")) (Var "12370" "indices")) False (TpVar "12380" "A"))))))) (Lam "12386" True "12388" "F" Nothing (Lam "12391" True "12393" "A" Nothing (Lam "12396" True "12398" "indices" Nothing (Lam "12407" False "12409" "alg" Nothing (Lam "12414" False "12416" "fix" Nothing (App (Var "12421" "fix") False (Var "12425" "alg")))))))) "12429",CmdDef Nothing (DefType "12431" "CVProduct'" (KdArrow (Tkk (KdParens "12445" (KdArrow (Tkk (KdParens "12446" (KdArrow (Tkt (TpVar "12447" "Indices")) (KdStar "12457")) "12459")) (KdArrow (Tkt (TpVar "12462" "Indices")) (KdStar "12472"))) "12474")) (KdArrow (Tkk (KdParens "12477" (KdArrow (Tkt (TpVar "12478" "Indices")) (KdStar "12488")) "12490")) (KdArrow (Tkt (TpVar "12493" "Indices")) (KdStar "12503")))) (TpLam "12509" "12511" "F" (Tkk (KdArrow (Tkk (KdParens "12515" (KdArrow (Tkt (TpVar "12516" "Indices")) (KdStar "12526")) "12528")) (KdArrow (Tkt (TpVar "12531" "Indices")) (KdStar "12541")))) (TpLam "12544" "12546" "X" (Tkk (KdArrow (Tkt (TpVar "12550" "Indices")) (KdStar "12560"))) (TpLam "12563" "12565" "indices" (Tkt (TpVar "12575" "Indices")) (TpApp (TpApp (TpVar "12588" "Sigma") (TpParens "12596" (TpAppt (TpApp (TpVar "12597" "F") (TpVar "12601" "X")) (Var "12603" "indices")) "12611")) (TpParens "12614" (TpLam "12615" "12617" "_" (Tkt (TpAppt (TpApp (TpVar "12621" "F") (TpVar "12625" "X")) (Var "12627" "indices"))) (TpArrow (TpAppt (TpVar "12636" "X") (Var "12638" "indices")) False (TpAppt (TpApp (TpVar "12648" "F") (TpVar "12652" "X")) (Var "12654" "indices")))) "12662")))))) "12663",CmdDef Nothing (DefType "12664" "CVF'" (KdArrow (Tkk (KdParens "12677" (KdArrow (Tkk (KdParens "12678" (KdArrow (Tkt (TpVar "12679" "Indices")) (KdStar "12689")) "12691")) (KdArrow (Tkt (TpVar "12694" "Indices")) (KdStar "12704"))) "12706")) (KdArrow (Tkk (KdParens "12709" (KdArrow (Tkt (TpVar "12710" "Indices")) (KdStar "12720")) "12722")) (KdArrow (Tkt (TpVar "12725" "Indices")) (KdStar "12735")))) (TpLam "12741" "12743" "F" (Tkk (KdArrow (Tkk (KdParens "12747" (KdArrow (Tkt (TpVar "12748" "Indices")) (KdStar "12758")) "12760")) (KdArrow (Tkt (TpVar "12763" "Indices")) (KdStar "12773")))) (TpApp (TpVar "12776" "CoendInd") (TpParens "12787" (TpApp (TpVar "12788" "CVProduct'") (TpVar "12801" "F")) "12803")))) "12804",CmdDef Nothing (DefType "12805" "CVFixIndM'" (KdArrow (Tkk (KdParens "12818" (KdArrow (Tkk (KdParens "12819" (KdArrow (Tkt (TpVar "12820" "Indices")) (KdStar "12830")) "12832")) (KdArrow (Tkt (TpVar "12835" "Indices")) (KdStar "12845"))) "12847")) (KdArrow (Tkt (TpVar "12850" "Indices")) (KdStar "12860"))) (TpLam "12866" "12868" "F" (Tkk (KdArrow (Tkk (KdParens "12872" (KdArrow (Tkt (TpVar "12873" "Indices")) (KdStar "12883")) "12885")) (KdArrow (Tkt (TpVar "12888" "Indices")) (KdStar "12898")))) (TpAppt (TpApp (TpVar "12901" "FixIndM") (TpParens "12911" (TpApp (TpVar "12912" "CVF'") (TpVar "12919" "F")) "12921")) (Parens "12922" (AppTp (Var "12923" "fmapCoend") (TpParens "12935" (TpApp (TpVar "12936" "CVProduct'") (TpVar "12949" "F")) "12951")) "12952")))) "12953",CmdDef Nothing (DefTerm "12955" "cvOutFixIndM'" (Just (TpAbs "12975" True "12977" "F" (Tkk (KdArrow (Tkk (KdParens "12981" (KdArrow (Tkt (TpVar "12982" "Indices")) (KdStar "12992")) "12994")) (KdArrow (Tkt (TpVar "12997" "Indices")) (KdStar "13007")))) (TpAbs "13010" True "13012" "fmap" (Tkt (TpApp (TpVar "13019" "Functor") (TpVar "13029" "F"))) (TpAbs "13032" True "13034" "indices" (Tkt (TpVar "13044" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "13057" "CVFixIndM'") (TpVar "13070" "F")) (Var "13072" "indices")) False (TpAppt (TpApp (TpVar "13082" "F") (TpParens "13086" (TpApp (TpVar "13087" "CVFixIndM'") (TpVar "13100" "F")) "13102")) (Var "13103" "indices"))))))) (Lam "13115" True "13117" "F" Nothing (Lam "13120" True "13122" "fmap" Nothing (Lam "13128" True "13130" "indices" Nothing (Lam "13139" False "13141" "v" Nothing (App (AppTp (App (App (AppTp (AppTp (Var "13144" "indCoend") (TpParens "13159" (TpApp (TpVar "13160" "CVProduct'") (TpVar "13173" "F")) "13175")) (TpParens "13182" (TpAppt (TpApp (TpVar "13183" "FixIndM") (TpParens "13193" (TpApp (TpVar "13194" "CoendInd") (TpParens "13205" (TpApp (TpVar "13206" "CVProduct'") (TpVar "13219" "F")) "13221")) "13222")) (Parens "13223" (AppTp (Var "13224" "fmapCoend") (TpParens "13236" (TpApp (TpVar "13237" "CVProduct'") (TpVar "13250" "F")) "13252")) "13253")) "13254")) True (Var "13260" "indices")) False (Parens "13268" (App (App (App (Var "13269" "outFixIndM") True (Parens "13281" (AppTp (Var "13282" "fmapCoend") (TpParens "13294" (TpApp (TpVar "13295" "CVProduct'") (TpVar "13308" "F")) "13310")) "13311")) True (Var "13313" "indices")) False (Var "13321" "v")) "13323")) (TpParens "13331" (TpLam "13332" "13334" "indices" (Tkt (TpVar "13344" "Indices")) (TpLam "13353" "13355" "_" (Tkt (TpAppt (TpApp (TpApp (TpVar "13359" "CoendInd") (TpParens "13370" (TpApp (TpVar "13371" "CVProduct'") (TpVar "13384" "F")) "13386")) (TpParens "13389" (TpApp (TpVar "13390" "CVFixIndM'") (TpVar "13403" "F")) "13405")) (Var "13406" "indices"))) (TpAppt (TpApp (TpVar "13423" "F") (TpParens "13427" (TpApp (TpVar "13428" "CVFixIndM'") (TpVar "13441" "F")) "13443")) (Var "13444" "indices")))) "13452")) False (Parens "13454" (Lam "13455" True "13457" "R" Nothing (Lam "13460" True "13462" "indices" Nothing (Lam "13471" True "13473" "c" Nothing (Lam "13476" False "13478" "v" Nothing (App (App (App (Var "13481" "cast") True (Parens "13487" (App (Var "13488" "fmap") True (Var "13494" "c")) "13496")) True (Var "13498" "indices")) False (Parens "13506" (App (Var "13507" "fst") False (Var "13511" "v")) "13513")))))) "13514"))))))) "13515",CmdDef Nothing (DefType "13517" "CVProduct" (KdArrow (Tkk (KdParens "13529" (KdArrow (Tkk (KdParens "13530" (KdArrow (Tkt (TpVar "13531" "Indices")) (KdStar "13541")) "13543")) (KdArrow (Tkt (TpVar "13546" "Indices")) (KdStar "13556"))) "13558")) (KdArrow (Tkk (KdParens "13561" (KdArrow (Tkt (TpVar "13562" "Indices")) (KdStar "13572")) "13574")) (KdArrow (Tkt (TpVar "13577" "Indices")) (KdStar "13587")))) (TpLam "13593" "13595" "F" (Tkk (KdArrow (Tkk (KdParens "13599" (KdArrow (Tkt (TpVar "13600" "Indices")) (KdStar "13610")) "13612")) (KdArrow (Tkt (TpVar "13615" "Indices")) (KdStar "13625")))) (TpLam "13628" "13630" "X" (Tkk (KdArrow (Tkt (TpVar "13634" "Indices")) (KdStar "13644"))) (TpLam "13647" "13649" "indices" (Tkt (TpVar "13659" "Indices")) (TpApp (TpApp (TpVar "13668" "Product") (TpParens "13682" (TpAppt (TpApp (TpVar "13683" "F") (TpVar "13687" "X")) (Var "13689" "indices")) "13697")) (TpParens "13704" (TpIota "13705" "13707" "o" (TpAbs "13711" True "13713" "indices" (Tkt (TpVar "13723" "Indices")) (TpArrow (TpAppt (TpVar "13732" "X") (Var "13734" "indices")) False (TpAppt (TpApp (TpVar "13744" "F") (TpVar "13748" "X")) (Var "13750" "indices")))) (TpEq "13759" (Var "13760" "o") (Var "13764" "cvOutFixIndM'") "13778")) "13779")))))) "13780",CmdDef Nothing (DefType "13781" "CVF" (KdArrow (Tkk (KdParens "13788" (KdArrow (Tkk (KdParens "13789" (KdArrow (Tkt (TpVar "13790" "Indices")) (KdStar "13800")) "13802")) (KdArrow (Tkt (TpVar "13805" "Indices")) (KdStar "13815"))) "13817")) (KdArrow (Tkk (KdParens "13820" (KdArrow (Tkt (TpVar "13821" "Indices")) (KdStar "13831")) "13833")) (KdArrow (Tkt (TpVar "13836" "Indices")) (KdStar "13846")))) (TpLam "13852" "13854" "F" (Tkk (KdArrow (Tkk (KdParens "13858" (KdArrow (Tkt (TpVar "13859" "Indices")) (KdStar "13869")) "13871")) (KdArrow (Tkt (TpVar "13874" "Indices")) (KdStar "13884")))) (TpApp (TpVar "13887" "CoendInd") (TpParens "13898" (TpApp (TpVar "13899" "CVProduct") (TpVar "13911" "F")) "13913")))) "13914",CmdDef Nothing (DefType "13915" "CVFixIndM" (KdAbs "13927" "13929" "F" (Tkk (KdArrow (Tkk (KdParens "13933" (KdArrow (Tkt (TpVar "13934" "Indices")) (KdStar "13944")) "13946")) (KdArrow (Tkt (TpVar "13949" "Indices")) (KdStar "13959")))) (KdArrow (Tkt (TpApp (TpVar "13962" "Functor") (TpVar "13972" "F"))) (KdArrow (Tkt (TpVar "13976" "Indices")) (KdStar "13986")))) (TpLam "13992" "13994" "F" (Tkk (KdArrow (Tkk (KdParens "13998" (KdArrow (Tkt (TpVar "13999" "Indices")) (KdStar "14009")) "14011")) (KdArrow (Tkt (TpVar "14014" "Indices")) (KdStar "14024")))) (TpLam "14027" "14029" "fmap" (Tkt (TpApp (TpVar "14036" "Functor") (TpVar "14046" "F"))) (TpAppt (TpApp (TpVar "14053" "FixIndM") (TpParens "14063" (TpApp (TpVar "14064" "CVF") (TpVar "14070" "F")) "14072")) (Parens "14073" (AppTp (Var "14074" "fmapCoend") (TpParens "14086" (TpApp (TpVar "14087" "CVProduct") (TpVar "14099" "F")) "14101")) "14102"))))) "14103",CmdDef Nothing (DefTerm "14105" "cvOutFixIndM" (Just (TpAbs "14124" True "14126" "F" (Tkk (KdArrow (Tkk (KdParens "14130" (KdArrow (Tkt (TpVar "14131" "Indices")) (KdStar "14141")) "14143")) (KdArrow (Tkt (TpVar "14146" "Indices")) (KdStar "14156")))) (TpAbs "14159" True "14161" "fmap" (Tkt (TpApp (TpVar "14168" "Functor") (TpVar "14178" "F"))) (TpAbs "14181" True "14183" "indices" (Tkt (TpVar "14193" "Indices")) (TpArrow (TpAppt (TpAppt (TpApp (TpVar "14206" "CVFixIndM") (TpVar "14218" "F")) (Var "14220" "fmap")) (Var "14225" "indices")) False (TpAppt (TpApp (TpVar "14235" "F") (TpParens "14239" (TpAppt (TpApp (TpVar "14240" "CVFixIndM") (TpVar "14252" "F")) (Var "14254" "fmap")) "14259")) (Var "14260" "indices"))))))) (Lam "14272" True "14274" "F" Nothing (Lam "14277" True "14279" "fmap" Nothing (Lam "14285" True "14287" "indices" Nothing (Lam "14296" False "14298" "v" Nothing (App (AppTp (App (App (AppTp (AppTp (Var "14301" "indCoend") (TpParens "14316" (TpApp (TpVar "14317" "CVProduct") (TpVar "14329" "F")) "14331")) (TpParens "14338" (TpAppt (TpApp (TpVar "14339" "FixIndM") (TpParens "14349" (TpApp (TpVar "14350" "CoendInd") (TpParens "14361" (TpApp (TpVar "14362" "CVProduct") (TpVar "14374" "F")) "14376")) "14377")) (Parens "14378" (AppTp (Var "14379" "fmapCoend") (TpParens "14391" (TpApp (TpVar "14392" "CVProduct") (TpVar "14404" "F")) "14406")) "14407")) "14408")) True (Var "14414" "indices")) False (Parens "14426" (App (App (App (Var "14427" "outFixIndM") True (Parens "14439" (AppTp (Var "14440" "fmapCoend") (TpParens "14452" (TpApp (TpVar "14453" "CVProduct") (TpVar "14465" "F")) "14467")) "14468")) True (Var "14470" "indices")) False (Var "14478" "v")) "14480")) (TpParens "14487" (TpLam "14488" "14490" "indices" (Tkt (TpVar "14500" "Indices")) (TpLam "14509" "14511" "_" (Tkt (TpAppt (TpApp (TpApp (TpVar "14515" "CoendInd") (TpParens "14526" (TpApp (TpVar "14527" "CVProduct") (TpVar "14539" "F")) "14541")) (TpParens "14544" (TpAppt (TpApp (TpVar "14545" "CVFixIndM") (TpVar "14557" "F")) (Var "14559" "fmap")) "14564")) (Var "14565" "indices"))) (TpAppt (TpApp (TpVar "14582" "F") (TpParens "14586" (TpAppt (TpApp (TpVar "14587" "CVFixIndM") (TpVar "14599" "F")) (Var "14601" "fmap")) "14606")) (Var "14607" "indices")))) "14615")) False (Parens "14620" (Lam "14621" True "14623" "R" Nothing (Lam "14626" True "14628" "indices" Nothing (Lam "14637" True "14639" "c" Nothing (Lam "14642" False "14644" "v" Nothing (App (App (App (Var "14647" "cast") True (Parens "14653" (App (Var "14654" "fmap") True (Var "14660" "c")) "14662")) True (Var "14664" "indices")) False (Parens "14672" (App (Var "14673" "fst") False (Var "14677" "v")) "14679")))))) "14680"))))))) "14681",CmdDef Nothing (DefTerm "14683" "cvInFixIndM" (Just (TpAbs "14701" True "14703" "F" (Tkk (KdArrow (Tkk (KdParens "14707" (KdArrow (Tkt (TpVar "14708" "Indices")) (KdStar "14718")) "14720")) (KdArrow (Tkt (TpVar "14723" "Indices")) (KdStar "14733")))) (TpAbs "14736" True "14738" "fmap" (Tkt (TpApp (TpVar "14745" "Functor") (TpVar "14755" "F"))) (TpAbs "14758" True "14760" "indices" (Tkt (TpVar "14770" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "14783" "F") (TpParens "14787" (TpAppt (TpApp (TpVar "14788" "CVFixIndM") (TpVar "14800" "F")) (Var "14802" "fmap")) "14807")) (Var "14808" "indices")) False (TpAppt (TpAppt (TpApp (TpVar "14818" "CVFixIndM") (TpVar "14830" "F")) (Var "14832" "fmap")) (Var "14837" "indices"))))))) (Lam "14849" True "14851" "F" Nothing (Lam "14854" True "14856" "fmap" Nothing (Lam "14862" True "14864" "indices" Nothing (Lam "14873" False "14875" "fcv" Nothing (App (App (App (Var "14880" "inFixIndM") True (Parens "14891" (AppTp (Var "14892" "fmapCoend") (TpParens "14904" (TpApp (TpVar "14905" "CVProduct") (TpVar "14917" "F")) "14919")) "14920")) True (Var "14922" "indices")) False (Parens "14934" (App (App (App (AppTp (AppTp (AppTp (Var "14935" "intrCoendInd") (TpParens "14950" (TpApp (TpVar "14951" "CVProduct") (TpVar "14963" "F")) "14965")) (TpParens "14968" (TpAppt (TpApp (TpVar "14969" "CVFixIndM") (TpVar "14981" "F")) (Var "14983" "fmap")) "14988")) (TpParens "14991" (TpAppt (TpApp (TpVar "14992" "CVFixIndM") (TpVar "15004" "F")) (Var "15006" "fmap")) "15011")) True (Var "15019" "indices")) True (IotaPair "15028" (Lam "15029" True "15031" "indices" Nothing (Lam "15040" False "15042" "x" Nothing (Var "15045" "x"))) (Beta "15048" Nothing Nothing) Nothing "15050")) False (Parens "15057" (App (App (Var "15058" "sigma") False (Var "15064" "fcv")) False (IotaPair "15068" (App (Var "15069" "cvOutFixIndM") True (Var "15083" "fmap")) (Beta "15089" Nothing (Just (PosTerm (Var "15091" "cvOutFixIndM") "15104"))) Nothing "15105")) "15106")) "15107"))))))) "15108",CmdDef Nothing (DefTerm "15110" "cvIndFixIndM" (Just (TpAbs "15129" True "15131" "F" (Tkk (KdArrow (Tkk (KdParens "15135" (KdArrow (Tkt (TpVar "15136" "Indices")) (KdStar "15146")) "15148")) (KdArrow (Tkt (TpVar "15151" "Indices")) (KdStar "15161")))) (TpAbs "15164" True "15166" "fmap" (Tkt (TpApp (TpVar "15173" "Functor") (TpVar "15183" "F"))) (TpAbs "15190" True "15192" "indices" (Tkt (TpVar "15202" "Indices")) (TpAbs "15211" False "15213" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "15217" "CVFixIndM") (TpVar "15229" "F")) (Var "15231" "fmap")) (Var "15236" "indices"))) (TpAbs "15249" True "15251" "Q" (Tkk (KdAbs "15255" "15257" "indices" (Tkt (TpVar "15267" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "15276" "CVFixIndM") (TpVar "15288" "F")) (Var "15290" "fmap")) (Var "15295" "indices"))) (KdStar "15305")))) (TpArrow (TpParens "15312" (TpAbs "15313" True "15315" "R" (Tkk (KdArrow (Tkt (TpVar "15319" "Indices")) (KdStar "15329"))) (TpAbs "15332" True "15334" "c" (Tkt (TpApp (TpApp (TpVar "15338" "Cast") (TpVar "15345" "R")) (TpParens "15349" (TpAppt (TpApp (TpVar "15350" "CVFixIndM") (TpVar "15362" "F")) (Var "15364" "fmap")) "15369"))) (TpArrow (TpParens "15377" (TpIota "15378" "15380" "out" (TpAbs "15386" True "15388" "indices" (Tkt (TpVar "15398" "Indices")) (TpArrow (TpAppt (TpVar "15407" "R") (Var "15409" "indices")) False (TpAppt (TpApp (TpVar "15419" "F") (TpVar "15423" "R")) (Var "15425" "indices")))) (TpEq "15434" (Var "15435" "out") (Var "15441" "cvOutFixIndM") "15454")) "15455") True (TpArrow (TpParens "15464" (TpAbs "15465" True "15467" "indices" (Tkt (TpVar "15477" "Indices")) (TpAbs "15486" False "15488" "r" (Tkt (TpAppt (TpVar "15492" "R") (Var "15494" "indices"))) (TpAppt (TpAppt (TpVar "15503" "Q") (Var "15505" "indices")) (Parens "15513" (App (App (App (Var "15514" "cast") True (Var "15520" "c")) True (Var "15523" "indices")) False (Var "15531" "r")) "15533")))) "15534") False (TpAbs "15543" True "15545" "indices" (Tkt (TpVar "15555" "Indices")) (TpAbs "15564" False "15566" "gr" (Tkt (TpAppt (TpApp (TpVar "15571" "F") (TpVar "15575" "R")) (Var "15577" "indices"))) (TpAppt (TpAppt (TpVar "15592" "Q") (Var "15594" "indices")) (Parens "15602" (App (App (App (Var "15603" "cvInFixIndM") True (Var "15616" "fmap")) True (Var "15622" "indices")) False (Parens "15630" (App (App (App (Var "15631" "cast") True (Parens "15637" (App (Var "15638" "fmap") True (Var "15644" "c")) "15646")) True (Var "15648" "indices")) False (Var "15656" "gr")) "15659")) "15660")))))))) "15661") False (TpAppt (TpAppt (TpVar "15668" "Q") (Var "15670" "indices")) (Var "15678" "e"))))))))) (Lam "15684" True "15686" "F" Nothing (Lam "15689" True "15691" "fmap" Nothing (Lam "15697" True "15699" "indices" Nothing (Lam "15708" False "15710" "e" Nothing (Lam "15713" True "15715" "Q" Nothing (Lam "15718" False "15720" "prf" Nothing (App (AppTp (App (App (App (Var "15729" "indFixIndM") True (Parens "15741" (AppTp (Var "15742" "fmapCoend") (TpParens "15754" (TpApp (TpVar "15755" "CVProduct") (TpVar "15767" "F")) "15769")) "15770")) True (Var "15772" "indices")) False (Var "15780" "e")) (TpVar "15784" "Q")) False (Parens "15792" (Lam "15793" True "15795" "R" Nothing (Lam "15798" True "15800" "i" Nothing (Lam "15803" False "15805" "ih" Nothing (Lam "15809" True "15811" "indices" Nothing (Lam "15820" False "15822" "gr" Nothing (Theta "15834" (AbstractVars ["indices","gr"]) (Parens "15848" (App (App (AppTp (AppTp (Var "15849" "indCoend") (TpParens "15860" (TpApp (TpVar "15861" "CVProduct") (TpVar "15873" "F")) "15875")) (TpVar "15878" "R")) True (Var "15881" "indices")) False (Var "15889" "gr")) "15892") [Lterm False (Parens "15903" (Lam "15904" True "15906" "R'" Nothing (Lam "15910" True "15912" "indices" Nothing (Lam "15921" True "15923" "i2" Nothing (Lam "15927" False "15929" "fr" Nothing (Theta "15933" (AbstractVars ["fr"]) (Parens "15939" (App (Var "15940" "SigmaInd") False (Var "15949" "fr")) "15952") [Lterm False (Parens "15965" (Lam "15966" False "15968" "a" Nothing (Lam "15971" False "15973" "b" Nothing (Rho "15976" False Nothing (IotaProj (Var "15978" "b") "2" "15981") Nothing (App (App (App (App (App (AppTp (Var "15984" "prf") (TpVar "15990" "R'")) True (IotaPair "16008" (Lam "16009" True "16011" "indices" Nothing (Lam "16020" False "16022" "r" Nothing (App (App (App (Var "16025" "cast") True (Var "16031" "i")) True (Var "16034" "indices")) False (Parens "16042" (App (App (App (Var "16043" "cast") True (Var "16049" "i2")) True (Var "16053" "indices")) False (Var "16061" "r")) "16063")))) (Beta "16065" Nothing Nothing) Nothing "16067")) True (Var "16069" "b")) False (Parens "16085" (Lam "16086" True "16088" "indices" Nothing (Lam "16097" False "16099" "r'" Nothing (App (App (Var "16103" "ih") True (Var "16107" "indices")) False (Parens "16115" (App (App (App (Var "16116" "cast") True (Var "16122" "i2")) True (Var "16126" "indices")) False (Var "16134" "r'")) "16137")))) "16138")) True (Var "16140" "indices")) False (Var "16148" "a"))))) "16150")]))))) "16151")])))))) "16152"))))))))) "16153",CmdDef Nothing (DefTerm "16155" "lambek" (Just (TpAbs "16168" True "16170" "F" (Tkk (KdArrow (Tkk (KdParens "16174" (KdArrow (Tkt (TpVar "16175" "Indices")) (KdStar "16185")) "16187")) (KdArrow (Tkt (TpVar "16190" "Indices")) (KdStar "16200")))) (TpAbs "16203" True "16205" "fmap" (Tkt (TpApp (TpVar "16212" "Functor") (TpVar "16222" "F"))) (TpAbs "16229" True "16231" "indices" (Tkt (TpVar "16241" "Indices")) (TpAbs "16250" False "16252" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "16256" "CVFixIndM") (TpVar "16268" "F")) (Var "16270" "fmap")) (Var "16275" "indices"))) (TpEq "16288" (App (Var "16289" "cvInFixIndM") False (Parens "16301" (App (Var "16302" "cvOutFixIndM") False (Var "16315" "e")) "16317")) (Var "16320" "e") "16322")))))) (Lam "16327" True "16329" "F" Nothing (Lam "16332" True "16334" "fmap" Nothing (Lam "16340" True "16342" "indices" Nothing (Lam "16351" False "16353" "e" Nothing (App (AppTp (App (App (App (AppTp (Var "16356" "cvIndFixIndM") (TpVar "16371" "F")) True (Var "16374" "fmap")) True (Var "16380" "indices")) False (Var "16388" "e")) (TpParens "16396" (TpLam "16397" "16399" "indices" (Tkt (TpVar "16409" "Indices")) (TpLam "16418" "16420" "e" (Tkt (TpAppt (TpAppt (TpApp (TpVar "16424" "CVFixIndM") (TpVar "16436" "F")) (Var "16438" "fmap")) (Var "16443" "indices"))) (TpEq "16461" (App (Var "16462" "cvInFixIndM") False (Parens "16474" (App (Var "16475" "cvOutFixIndM") False (Var "16488" "e")) "16490")) (Var "16493" "e") "16495"))) "16496")) False (Parens "16501" (Lam "16502" True "16504" "R" Nothing (Lam "16507" True "16509" "i" Nothing (Lam "16512" True "16514" "out" Nothing (Lam "16519" False "16521" "ih" Nothing (Lam "16525" True "16527" "indices" Nothing (Lam "16536" False "16538" "gr" Nothing (Beta "16542" Nothing Nothing))))))) "16544"))))))) "16545"] "16545"
  
  
  -- src/templates/MendlerSimple.ced
  templateMendlerSimple = Module [] "1" "8" "MendlerSimple" [Param "22" True "23" "Indices" (Tkk (KdStar "33")) "35"] [CmdDef Nothing (DefType "38" "Top" (KdStar "44") (TpEq "48" (Beta "49" Nothing Nothing) (Beta "53" Nothing Nothing) "55")) "56",CmdDef Nothing (DefType "58" "Cast" (KdArrow (Tkk (KdParens "65" (KdArrow (Tkt (TpVar "66" "Indices")) (KdStar "76")) "78")) (KdArrow (Tkk (KdParens "81" (KdArrow (Tkt (TpVar "82" "Indices")) (KdStar "92")) "94")) (KdStar "97"))) (TpLam "101" "103" "A" (Tkk (KdArrow (Tkt (TpVar "107" "Indices")) (KdStar "117"))) (TpLam "120" "122" "B" (Tkk (KdArrow (Tkt (TpVar "126" "Indices")) (KdStar "136"))) (TpIota "141" "143" "cast" (TpAbs "150" True "152" "indices" (Tkt (TpVar "162" "Indices")) (TpArrow (TpAppt (TpVar "171" "A") (Var "173" "indices")) False (TpAppt (TpVar "183" "B") (Var "185" "indices")))) (TpEq "194" (Var "195" "cast") (Lam "202" False "204" "x" Nothing (Var "207" "x")) "209"))))) "210",CmdDef Nothing (DefTerm "212" "cast" (Just (TpAbs "219" True "221" "A" (Tkk (KdArrow (Tkt (TpVar "225" "Indices")) (KdStar "235"))) (TpAbs "238" True "240" "B" (Tkk (KdArrow (Tkt (TpVar "244" "Indices")) (KdStar "254"))) (TpArrow (TpApp (TpApp (TpVar "257" "Cast") (TpVar "264" "A")) (TpVar "268" "B")) True (TpAbs "276" True "278" "indices" (Tkt (TpVar "288" "Indices")) (TpArrow (TpAppt (TpVar "297" "A") (Var "299" "indices")) False (TpAppt (TpVar "309" "B") (Var "311" "indices")))))))) (Lam "323" True "325" "A" Nothing (Lam "328" True "330" "B" Nothing (Lam "333" True "335" "c" Nothing (Phi "338" (IotaProj (Var "340" "c") "2" "343") (IotaProj (Var "346" "c") "1" "349") (Lam "351" False "353" "x" Nothing (Var "356" "x")) "358"))))) "359",CmdDef Nothing (DefType "361" "RecFunctor" (KdArrow (Tkk (KdParens "374" (KdArrow (Tkk (KdParens "375" (KdArrow (Tkt (TpVar "376" "Indices")) (KdStar "386")) "388")) (KdArrow (Tkt (TpVar "391" "Indices")) (KdStar "401"))) "403")) (KdStar "406")) (TpLam "412" "414" "F" (Tkk (KdArrow (Tkk (KdParens "418" (KdArrow (Tkt (TpVar "419" "Indices")) (KdStar "429")) "431")) (KdArrow (Tkt (TpVar "434" "Indices")) (KdStar "444")))) (TpAbs "447" True "449" "X" (Tkk (KdArrow (Tkt (TpVar "453" "Indices")) (KdStar "463"))) (TpAbs "466" True "468" "Y" (Tkk (KdArrow (Tkt (TpVar "472" "Indices")) (KdStar "482"))) (TpArrow (TpApp (TpApp (TpVar "489" "Cast") (TpVar "496" "X")) (TpVar "500" "Y")) True (TpApp (TpApp (TpVar "504" "Cast") (TpParens "511" (TpApp (TpVar "512" "F") (TpVar "516" "X")) "518")) (TpParens "521" (TpApp (TpVar "522" "F") (TpVar "526" "Y")) "528"))))))) "529",CmdDef Nothing (DefType "531" "Rec" (KdArrow (Tkk (KdParens "537" (KdArrow (Tkk (KdParens "538" (KdArrow (Tkt (TpVar "539" "Indices")) (KdStar "549")) "551")) (KdArrow (Tkt (TpVar "554" "Indices")) (KdStar "564"))) "566")) (KdArrow (Tkt (TpVar "569" "Indices")) (KdStar "579"))) (TpLam "585" "587" "F" (Tkk (KdArrow (Tkk (KdParens "591" (KdArrow (Tkt (TpVar "592" "Indices")) (KdStar "602")) "604")) (KdArrow (Tkt (TpVar "607" "Indices")) (KdStar "617")))) (TpLam "620" "622" "indices" (Tkt (TpVar "632" "Indices")) (TpAbs "645" True "647" "X" (Tkk (KdArrow (Tkt (TpVar "651" "Indices")) (KdStar "661"))) (TpArrow (TpApp (TpApp (TpVar "664" "Cast") (TpParens "671" (TpApp (TpVar "672" "F") (TpVar "676" "X")) "678")) (TpVar "681" "X")) True (TpAppt (TpVar "685" "X") (Var "687" "indices"))))))) "695",CmdDef Nothing (DefTerm "698" "recCast" (Just (TpAbs "708" True "710" "F" (Tkk (KdArrow (Tkk (KdParens "714" (KdArrow (Tkt (TpVar "715" "Indices")) (KdStar "725")) "727")) (KdArrow (Tkt (TpVar "730" "Indices")) (KdStar "740")))) (TpAbs "743" True "745" "X" (Tkk (KdArrow (Tkt (TpVar "749" "Indices")) (KdStar "759"))) (TpArrow (TpApp (TpApp (TpVar "766" "Cast") (TpParens "773" (TpApp (TpVar "774" "F") (TpVar "778" "X")) "780")) (TpVar "783" "X")) True (TpApp (TpApp (TpVar "787" "Cast") (TpParens "794" (TpApp (TpVar "795" "Rec") (TpVar "801" "F")) "803")) (TpVar "806" "X")))))) (Lam "812" True "814" "F" Nothing (Lam "817" True "819" "X" Nothing (Lam "822" True "824" "c" Nothing (IotaPair "827" (Lam "828" True "830" "indices" Nothing (Lam "839" False "841" "a" Nothing (App (AppTp (Var "844" "a") (TpVar "848" "X")) True (Var "851" "c")))) (Beta "854" Nothing Nothing) Nothing "856"))))) "857",CmdDef Nothing (DefTerm "859" "recIn" (Just (TpAbs "867" True "869" "F" (Tkk (KdArrow (Tkk (KdParens "873" (KdArrow (Tkt (TpVar "874" "Indices")) (KdStar "884")) "886")) (KdArrow (Tkt (TpVar "889" "Indices")) (KdStar "899")))) (TpArrow (TpApp (TpVar "902" "RecFunctor") (TpVar "915" "F")) True (TpApp (TpApp (TpVar "923" "Cast") (TpParens "930" (TpApp (TpVar "931" "F") (TpParens "935" (TpApp (TpVar "936" "Rec") (TpVar "942" "F")) "944")) "945")) (TpParens "948" (TpApp (TpVar "949" "Rec") (TpVar "955" "F")) "957"))))) (Lam "962" True "964" "F" Nothing (Lam "967" True "969" "fmap" Nothing (IotaPair "979" (Lam "980" True "982" "indices" Nothing (Lam "991" False "993" "a" Nothing (Lam "996" True "998" "X" Nothing (Lam "1001" True "1003" "c" Nothing (App (App (App (Var "1006" "cast") True (Var "1012" "c")) True (Var "1015" "indices")) False (Parens "1023" (App (App (App (Var "1024" "cast") True (Parens "1030" (App (Var "1031" "fmap") True (Parens "1037" (App (Var "1038" "recCast") True (Var "1047" "c")) "1049")) "1050")) True (Var "1052" "indices")) False (Var "1060" "a")) "1062")))))) (Beta "1064" Nothing Nothing) Nothing "1066")))) "1067",CmdDef Nothing (DefTerm "1069" "recOut" (Just (TpAbs "1078" True "1080" "F" (Tkk (KdArrow (Tkk (KdParens "1084" (KdArrow (Tkt (TpVar "1085" "Indices")) (KdStar "1095")) "1097")) (KdArrow (Tkt (TpVar "1100" "Indices")) (KdStar "1110")))) (TpArrow (TpApp (TpVar "1113" "RecFunctor") (TpVar "1126" "F")) True (TpApp (TpApp (TpVar "1140" "Cast") (TpParens "1147" (TpApp (TpVar "1148" "Rec") (TpVar "1154" "F")) "1156")) (TpParens "1159" (TpApp (TpVar "1160" "F") (TpParens "1164" (TpApp (TpVar "1165" "Rec") (TpVar "1171" "F")) "1173")) "1174"))))) (Lam "1179" True "1181" "F" Nothing (Lam "1184" True "1186" "fmap" Nothing (IotaPair "1192" (Lam "1193" True "1195" "indices" Nothing (Lam "1204" False "1206" "a" Nothing (App (Var "1209" "a") True (Parens "1212" (App (Var "1213" "fmap") True (Parens "1219" (App (Var "1220" "recIn") True (Var "1227" "fmap")) "1232")) "1233")))) (Beta "1235" Nothing Nothing) Nothing "1237")))) "1238",CmdDef Nothing (DefType "1240" "FixMF" (KdAbs "1248" "1250" "F" (Tkk (KdArrow (Tkk (KdParens "1254" (KdArrow (Tkt (TpVar "1255" "Indices")) (KdStar "1265")) "1267")) (KdArrow (Tkt (TpVar "1270" "Indices")) (KdStar "1280")))) (KdArrow (Tkt (TpApp (TpVar "1283" "RecFunctor") (TpVar "1296" "F"))) (KdArrow (Tkk (KdParens "1300" (KdArrow (Tkt (TpVar "1301" "Indices")) (KdStar "1311")) "1313")) (KdArrow (Tkt (TpVar "1316" "Indices")) (KdStar "1326"))))) (TpLam "1332" "1334" "F" (Tkk (KdArrow (Tkk (KdParens "1338" (KdArrow (Tkt (TpVar "1339" "Indices")) (KdStar "1349")) "1351")) (KdArrow (Tkt (TpVar "1354" "Indices")) (KdStar "1364")))) (TpLam "1367" "1369" "fm" (Tkt (TpApp (TpVar "1374" "RecFunctor") (TpVar "1387" "F"))) (TpLam "1394" "1396" "FixM" (Tkk (KdArrow (Tkt (TpVar "1403" "Indices")) (KdStar "1413"))) (TpLam "1416" "1418" "indices" (Tkt (TpVar "1428" "Indices")) (TpIota "1444" "1446" "x" (TpVar "1450" "Top") (TpAbs "1455" True "1457" "X" (Tkk (KdArrow (Tkt (TpVar "1461" "Top")) (KdArrow (Tkt (TpVar "1467" "Indices")) (KdStar "1477")))) (TpArrow (TpParens "1488" (TpIota "1489" "1491" "alg" (TpVar "1497" "Top") (TpAbs "1511" True "1513" "R" (Tkk (KdArrow (Tkt (TpVar "1517" "Indices")) (KdStar "1527"))) (TpArrow (TpApp (TpApp (TpVar "1539" "Cast") (TpVar "1546" "R")) (TpVar "1550" "FixM")) True (TpArrow (TpParens "1566" (TpIota "1567" "1569" "o" (TpAbs "1573" True "1575" "indices" (Tkt (TpVar "1585" "Indices")) (TpArrow (TpAppt (TpVar "1594" "R") (Var "1596" "indices")) False (TpAppt (TpApp (TpVar "1606" "F") (TpVar "1610" "R")) (Var "1612" "indices")))) (TpEq "1621" (Var "1622" "o") (Lam "1626" False "1628" "d" Nothing (App (Var "1631" "d") False (Parens "1633" (Lam "1634" False "1636" "p" Nothing (Lam "1639" False "1641" "d" Nothing (Var "1644" "d"))) "1646"))) "1647")) "1648") True (TpArrow (TpParens "1660" (TpIota "1661" "1663" "ih" (TpAbs "1668" True "1670" "indices" (Tkt (TpVar "1680" "Indices")) (TpAbs "1689" False "1691" "r" (Tkt (TpAppt (TpVar "1695" "R") (Var "1697" "indices"))) (TpAppt (TpAppt (TpVar "1706" "X") (Beta "1708" Nothing (Just (PosTerm (Var "1710" "r") "1712")))) (Var "1713" "indices")))) (TpEq "1722" (Var "1723" "ih") (Lam "1728" False "1730" "d" Nothing (App (Var "1733" "d") False (Var "1735" "alg"))) "1739")) "1740") False (TpAbs "1752" True "1754" "indices" (Tkt (TpVar "1764" "Indices")) (TpAbs "1782" False "1784" "x" (Tkt (TpAppt (TpApp (TpVar "1788" "F") (TpVar "1792" "R")) (Var "1794" "indices"))) (TpAppt (TpAppt (TpVar "1812" "X") (Beta "1814" Nothing (Just (PosTerm (Lam "1816" False "1818" "alg" Nothing (App (App (Var "1823" "alg") False (Parens "1827" (Lam "1828" False "1830" "d" Nothing (App (Var "1833" "d") False (Var "1835" "alg"))) "1839")) False (Var "1840" "x"))) "1842")))) (Var "1843" "indices"))))))))) "1851") False (TpAppt (TpAppt (TpVar "1862" "X") (Var "1864" "x")) (Var "1866" "indices")))))))))) "1874",CmdDef Nothing (DefType "1876" "FixM" (KdAbs "1883" "1885" "F" (Tkk (KdArrow (Tkk (KdParens "1889" (KdArrow (Tkt (TpVar "1890" "Indices")) (KdStar "1900")) "1902")) (KdArrow (Tkt (TpVar "1905" "Indices")) (KdStar "1915")))) (KdArrow (Tkt (TpApp (TpVar "1918" "RecFunctor") (TpVar "1931" "F"))) (KdArrow (Tkt (TpVar "1935" "Indices")) (KdStar "1945")))) (TpLam "1951" "1953" "F" (Tkk (KdArrow (Tkk (KdParens "1957" (KdArrow (Tkt (TpVar "1958" "Indices")) (KdStar "1968")) "1970")) (KdArrow (Tkt (TpVar "1973" "Indices")) (KdStar "1983")))) (TpLam "1986" "1988" "fm" (Tkt (TpApp (TpVar "1993" "RecFunctor") (TpVar "2006" "F"))) (TpApp (TpVar "2009" "Rec") (TpParens "2015" (TpAppt (TpApp (TpVar "2016" "FixMF") (TpVar "2024" "F")) (Var "2026" "fm")) "2029"))))) "2030",CmdDef Nothing (DefTerm "2032" "FixFmap" (Just (TpAbs "2046" True "2048" "F" (Tkk (KdArrow (Tkk (KdParens "2052" (KdArrow (Tkt (TpVar "2053" "Indices")) (KdStar "2063")) "2065")) (KdArrow (Tkt (TpVar "2068" "Indices")) (KdStar "2078")))) (TpAbs "2081" True "2083" "fm" (Tkt (TpApp (TpVar "2088" "RecFunctor") (TpVar "2101" "F"))) (TpApp (TpVar "2104" "RecFunctor") (TpParens "2117" (TpAppt (TpApp (TpVar "2118" "FixMF") (TpVar "2126" "F")) (Var "2128" "fm")) "2131"))))) (Lam "2136" True "2138" "F" Nothing (Lam "2141" True "2143" "fm" Nothing (Lam "2147" True "2149" "D" Nothing (Lam "2152" True "2154" "D'" Nothing (Lam "2158" True "2160" "c" Nothing (IotaPair "2167" (Lam "2168" True "2170" "indices" Nothing (Lam "2179" False "2181" "d" Nothing (IotaPair "2184" (IotaProj (Var "2185" "d") "1" "2188") (Lam "2190" True "2192" "X" Nothing (Lam "2195" False "2197" "alg" Nothing (App (AppTp (IotaProj (Var "2202" "d") "2" "2205") (TpVar "2208" "X")) False (IotaPair "2216" (IotaProj (Var "2217" "alg") "1" "2222") (Lam "2224" True "2226" "R" Nothing (Lam "2229" True "2231" "reveal" Nothing (App (AppTp (IotaProj (Var "2239" "alg") "2" "2244") (TpVar "2247" "R")) True (IotaPair "2258" (Lam "2259" True "2261" "indices" Nothing (Lam "2270" False "2272" "r" Nothing (App (App (App (Var "2275" "cast") True (Var "2281" "c")) True (Var "2284" "indices")) False (Parens "2292" (App (App (App (Var "2293" "cast") True (Var "2299" "reveal")) True (Var "2307" "indices")) False (Var "2315" "r")) "2317")))) (Beta "2319" Nothing Nothing) Nothing "2321")))) Nothing "2322")))) Nothing "2323"))) (Beta "2325" Nothing Nothing) Nothing "2327"))))))) "2328",CmdDef Nothing (DefTerm "2330" "inFixM" (Just (TpAbs "2343" True "2345" "F" (Tkk (KdArrow (Tkk (KdParens "2349" (KdArrow (Tkt (TpVar "2350" "Indices")) (KdStar "2360")) "2362")) (KdArrow (Tkt (TpVar "2365" "Indices")) (KdStar "2375")))) (TpAbs "2378" True "2380" "fm" (Tkt (TpApp (TpVar "2385" "RecFunctor") (TpVar "2398" "F"))) (TpAbs "2405" True "2407" "indices" (Tkt (TpVar "2417" "Indices")) (TpArrow (TpAppt (TpApp (TpAppt (TpApp (TpVar "2426" "FixMF") (TpVar "2434" "F")) (Var "2436" "fm")) (TpParens "2441" (TpAppt (TpApp (TpVar "2442" "FixM") (TpVar "2449" "F")) (Var "2451" "fm")) "2454")) (Var "2455" "indices")) False (TpAppt (TpAppt (TpApp (TpVar "2465" "FixM") (TpVar "2472" "F")) (Var "2474" "fm")) (Var "2477" "indices"))))))) (Lam "2489" True "2491" "F" Nothing (Lam "2494" True "2496" "fm" Nothing (App (Var "2500" "cast") True (Parens "2506" (App (Var "2507" "recIn") True (Parens "2514" (App (Var "2515" "FixFmap") True (Var "2524" "fm")) "2527")) "2528"))))) "2529",CmdDef Nothing (DefTerm "2530" "outFixM" (Just (TpAbs "2540" True "2542" "F" (Tkk (KdArrow (Tkk (KdParens "2546" (KdArrow (Tkt (TpVar "2547" "Indices")) (KdStar "2557")) "2559")) (KdArrow (Tkt (TpVar "2562" "Indices")) (KdStar "2572")))) (TpAbs "2575" True "2577" "fm" (Tkt (TpApp (TpVar "2582" "RecFunctor") (TpVar "2595" "F"))) (TpAbs "2602" True "2604" "indices" (Tkt (TpVar "2614" "Indices")) (TpArrow (TpAppt (TpAppt (TpApp (TpVar "2623" "FixM") (TpVar "2630" "F")) (Var "2632" "fm")) (Var "2635" "indices")) False (TpAppt (TpApp (TpAppt (TpApp (TpVar "2645" "FixMF") (TpVar "2653" "F")) (Var "2655" "fm")) (TpParens "2660" (TpAppt (TpApp (TpVar "2661" "FixM") (TpVar "2668" "F")) (Var "2670" "fm")) "2673")) (Var "2674" "indices"))))))) (Lam "2686" True "2688" "F" Nothing (Lam "2691" True "2693" "fm" Nothing (App (Var "2697" "cast") True (Parens "2703" (App (Var "2704" "recOut") True (Parens "2712" (App (Var "2713" "FixFmap") True (Var "2722" "fm")) "2725")) "2726"))))) "2727",CmdDef Nothing (DefTerm "2729" "inFix" (Just (TpAbs "2741" True "2743" "F" (Tkk (KdArrow (Tkk (KdParens "2747" (KdArrow (Tkt (TpVar "2748" "Indices")) (KdStar "2758")) "2760")) (KdArrow (Tkt (TpVar "2763" "Indices")) (KdStar "2773")))) (TpAbs "2776" True "2778" "fm" (Tkt (TpApp (TpVar "2783" "RecFunctor") (TpVar "2796" "F"))) (TpAbs "2803" True "2805" "indices" (Tkt (TpVar "2815" "Indices")) (TpArrow (TpAppt (TpApp (TpVar "2824" "F") (TpParens "2828" (TpAppt (TpApp (TpVar "2829" "FixM") (TpVar "2836" "F")) (Var "2838" "fm")) "2841")) (Var "2842" "indices")) False (TpAppt (TpAppt (TpApp (TpVar "2852" "FixM") (TpVar "2859" "F")) (Var "2861" "fm")) (Var "2864" "indices"))))))) (Lam "2876" True "2878" "F" Nothing (Lam "2881" True "2883" "fm" Nothing (Lam "2887" True "2889" "indices" Nothing (Lam "2898" False "2900" "d" Nothing (App (App (App (Var "2903" "inFixM") True (Var "2911" "fm")) True (Var "2915" "indices")) False (IotaPair "2925" (Beta "2926" Nothing (Just (PosTerm (Lam "2928" False "2930" "alg" Nothing (App (App (Var "2935" "alg") False (Parens "2939" (Lam "2940" False "2942" "d" Nothing (App (Var "2945" "d") False (Var "2947" "alg"))) "2951")) False (Var "2952" "d"))) "2954"))) (Lam "2959" True "2961" "X" Nothing (Lam "2964" False "2966" "alg" Nothing (App (App (App (App (App (AppTp (IotaProj (Var "2971" "alg") "2" "2976") (TpParens "2979" (TpAppt (TpApp (TpVar "2980" "FixM") (TpVar "2987" "F")) (Var "2989" "fm")) "2992")) True (IotaPair "2994" (Lam "2995" True "2997" "indices" Nothing (Lam "3006" False "3008" "d" Nothing (Var "3011" "d"))) (Beta "3014" Nothing Nothing) Nothing "3016")) True (IotaPair "3023" (Lam "3024" True "3026" "indices" Nothing (Lam "3035" False "3037" "d" Nothing (App (AppTp (IotaProj (Parens "3040" (App (App (App (Var "3041" "outFixM") True (Var "3050" "fm")) True (Var "3054" "indices")) False (Var "3062" "d")) "3064") "2" "3066") (TpParens "3069" (TpLam "3070" "3072" "x" (Tkt (TpVar "3076" "Top")) (TpApp (TpVar "3081" "F") (TpParens "3085" (TpAppt (TpApp (TpVar "3086" "FixM") (TpVar "3093" "F")) (Var "3095" "fm")) "3098"))) "3099")) False (IotaPair "3107" (Beta "3108" Nothing (Just (PosTerm (Lam "3110" False "3112" "e" Nothing (Lam "3115" False "3117" "d" Nothing (Var "3120" "d"))) "3122"))) (Lam "3124" True "3126" "X" Nothing (Lam "3129" True "3131" "reveal" Nothing (Lam "3139" True "3141" "p" Nothing (Lam "3144" False "3146" "e" Nothing (App (Var "3149" "cast") True (Parens "3155" (App (Var "3156" "fm") True (Var "3160" "reveal")) "3167")))))) Nothing "3168")))) (Beta "3178" Nothing (Just (PosTerm (Lam "3180" False "3182" "d" Nothing (App (Var "3185" "d") False (Parens "3187" (Lam "3188" False "3190" "e" Nothing (Lam "3193" False "3195" "d" Nothing (Var "3198" "d"))) "3200"))) "3201"))) Nothing "3202")) False (IotaPair "3208" (Lam "3209" True "3211" "indices" Nothing (Lam "3220" False "3222" "d" Nothing (App (AppTp (IotaProj (Parens "3225" (App (App (App (Var "3226" "outFixM") True (Var "3235" "fm")) True (Var "3239" "indices")) False (Var "3247" "d")) "3249") "2" "3251") (TpVar "3254" "X")) False (Var "3256" "alg")))) (Beta "3261" Nothing (Just (PosTerm (Lam "3263" False "3265" "d" Nothing (App (Var "3268" "d") False (Var "3270" "alg"))) "3274"))) Nothing "3275")) True (Var "3277" "indices")) False (Var "3285" "d")))) Nothing "3287"))))))) "3288",CmdDef Nothing (DefTerm "3290" "outFix" (Just (TpAbs "3303" True "3305" "F" (Tkk (KdArrow (Tkk (KdParens "3309" (KdArrow (Tkt (TpVar "3310" "Indices")) (KdStar "3320")) "3322")) (KdArrow (Tkt (TpVar "3325" "Indices")) (KdStar "3335")))) (TpAbs "3338" True "3340" "fm" (Tkt (TpApp (TpVar "3345" "RecFunctor") (TpVar "3358" "F"))) (TpAbs "3365" True "3367" "indices" (Tkt (TpVar "3377" "Indices")) (TpArrow (TpAppt (TpAppt (TpApp (TpVar "3386" "FixM") (TpVar "3393" "F")) (Var "3395" "fm")) (Var "3398" "indices")) False (TpAppt (TpApp (TpVar "3408" "F") (TpParens "3412" (TpAppt (TpApp (TpVar "3413" "FixM") (TpVar "3420" "F")) (Var "3422" "fm")) "3425")) (Var "3426" "indices"))))))) (Lam "3438" True "3440" "F" Nothing (Lam "3443" True "3445" "fm" Nothing (Lam "3449" True "3451" "indices" Nothing (Lam "3460" False "3462" "x" Nothing (App (AppTp (IotaProj (Parens "3465" (App (App (App (Var "3466" "outFixM") True (Var "3475" "fm")) True (Var "3479" "indices")) False (Var "3487" "x")) "3489") "2" "3491") (TpParens "3494" (TpLam "3495" "3497" "x" (Tkt (TpVar "3501" "Top")) (TpApp (TpVar "3506" "F") (TpParens "3510" (TpAppt (TpApp (TpVar "3511" "FixM") (TpVar "3518" "F")) (Var "3520" "fm")) "3523"))) "3524")) False (IotaPair "3529" (Beta "3530" Nothing (Just (PosTerm (Lam "3532" False "3534" "e" Nothing (Lam "3537" False "3539" "d" Nothing (Var "3542" "d"))) "3544"))) (Lam "3546" True "3548" "R" Nothing (Lam "3551" True "3553" "c" Nothing (Lam "3556" True "3558" "p" Nothing (Lam "3561" False "3563" "e" Nothing (App (Var "3566" "cast") True (Parens "3572" (App (Var "3573" "fm") True (Var "3577" "c")) "3579")))))) Nothing "3580"))))))) "3581",CmdDef Nothing (DefTerm "3584" "IndFixM'" (Just (TpAbs "3599" True "3601" "F" (Tkk (KdArrow (Tkk (KdParens "3605" (KdArrow (Tkt (TpVar "3606" "Indices")) (KdStar "3616")) "3618")) (KdArrow (Tkt (TpVar "3621" "Indices")) (KdStar "3631")))) (TpAbs "3638" True "3640" "fm" (Tkt (TpApp (TpVar "3645" "RecFunctor") (TpVar "3658" "F"))) (TpAbs "3665" True "3667" "indices" (Tkt (TpVar "3677" "Indices")) (TpAbs "3690" False "3692" "d" (Tkt (TpAppt (TpAppt (TpApp (TpVar "3696" "FixM") (TpVar "3703" "F")) (Var "3705" "fm")) (Var "3708" "indices"))) (TpAbs "3721" True "3723" "Q" (Tkk (KdAbs "3727" "3729" "indices" (Tkt (TpVar "3739" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "3748" "FixM") (TpVar "3755" "F")) (Var "3757" "fm")) (Var "3760" "indices"))) (KdStar "3770")))) (TpArrow (TpParens "3777" (TpIota "3778" "3780" "alg" (TpVar "3786" "Top") (TpAbs "3798" True "3800" "R" (Tkk (KdArrow (Tkt (TpVar "3804" "Indices")) (KdStar "3814"))) (TpAbs "3824" True "3826" "reveal" (Tkt (TpApp (TpApp (TpVar "3835" "Cast") (TpVar "3842" "R")) (TpParens "3846" (TpAppt (TpApp (TpVar "3847" "FixM") (TpVar "3854" "F")) (Var "3856" "fm")) "3859"))) (TpArrow (TpParens "3868" (TpIota "3869" "3871" "o" (TpAbs "3875" True "3877" "indices" (Tkt (TpVar "3887" "Indices")) (TpArrow (TpAppt (TpVar "3896" "R") (Var "3898" "indices")) False (TpAppt (TpApp (TpVar "3908" "F") (TpVar "3912" "R")) (Var "3914" "indices")))) (TpEq "3923" (Var "3924" "o") (Var "3928" "outFix") "3935")) "3936") True (TpArrow (TpParens "3946" (TpIota "3947" "3949" "ih" (TpAbs "3954" True "3956" "indices" (Tkt (TpVar "3966" "Indices")) (TpAbs "3975" False "3977" "r" (Tkt (TpAppt (TpVar "3981" "R") (Var "3983" "indices"))) (TpAppt (TpAppt (TpVar "4001" "Q") (Var "4003" "indices")) (Parens "4011" (App (App (App (Var "4012" "cast") True (Var "4018" "reveal")) True (Var "4026" "indices")) False (Var "4034" "r")) "4036")))) (TpEq "4038" (Var "4039" "ih") (Lam "4044" False "4046" "d" Nothing (App (Var "4049" "d") False (Var "4051" "alg"))) "4055")) "4056") False (TpAbs "4066" True "4068" "indices" (Tkt (TpVar "4078" "Indices")) (TpAbs "4094" False "4096" "x" (Tkt (TpAppt (TpApp (TpVar "4100" "F") (TpVar "4104" "R")) (Var "4106" "indices"))) (TpAppt (TpAppt (TpVar "4122" "Q") (Var "4124" "indices")) (Parens "4132" (App (App (App (Var "4133" "inFix") True (Var "4140" "fm")) True (Var "4144" "indices")) False (Parens "4152" (App (App (App (Var "4153" "cast") True (Parens "4159" (App (Var "4160" "fm") True (Var "4164" "reveal")) "4171")) True (Var "4173" "indices")) False (Var "4181" "x")) "4183")) "4184"))))))))) "4185") False (TpAppt (TpAppt (TpVar "4192" "Q") (Var "4194" "indices")) (Var "4202" "d"))))))))) (Lam "4208" True "4210" "F" Nothing (Lam "4213" True "4215" "fm" Nothing (Lam "4219" True "4221" "indices" Nothing (Lam "4230" False "4232" "d" Nothing (Lam "4235" True "4237" "Q" Nothing (Lam "4240" False "4242" "alg" Nothing (App (App (App (AppTp (IotaProj (Parens "4247" (App (App (App (Var "4248" "outFixM") True (Var "4257" "fm")) True (Var "4261" "indices")) False (Var "4269" "d")) "4271") "2" "4273") (TpParens "4280" (TpLam "4281" "4283" "d" (Tkt (TpVar "4287" "Top")) (TpLam "4292" "4294" "indices" (Tkt (TpVar "4304" "Indices")) (TpAbs "4322" True "4324" "d'" (Tkt (TpAppt (TpAppt (TpApp (TpVar "4329" "FixM") (TpVar "4336" "F")) (Var "4338" "fm")) (Var "4341" "indices"))) (TpAbs "4350" True "4352" "e" (Tkt (TpEq "4356" (Var "4357" "d'") (Var "4362" "d") "4364")) (TpAppt (TpAppt (TpVar "4366" "Q") (Var "4368" "indices")) (Parens "4376" (Phi "4377" (Var "4379" "e") (Var "4383" "d'") (Var "4387" "d") "4389") "4390")))))) "4391")) False (IotaPair "4396" (Beta "4397" Nothing (Just (PosTerm (Var "4399" "alg") "4403"))) (Lam "4405" True "4407" "R" Nothing (Lam "4410" True "4412" "reveal" Nothing (Lam "4420" True "4422" "out" Nothing (Lam "4427" False "4429" "ih" Nothing (Lam "4433" True "4435" "indices" Nothing (Lam "4444" False "4446" "d" Nothing (Lam "4449" True "4451" "d'" Nothing (Lam "4455" True "4457" "e" Nothing (App (App (App (App (App (AppTp (IotaProj (Var "4460" "alg") "2" "4465") (TpVar "4468" "R")) True (Var "4471" "reveal")) True (Var "4479" "out")) False (IotaPair "4489" (Lam "4490" True "4492" "indices" Nothing (Lam "4501" False "4503" "r" Nothing (App (App (App (App (IotaProj (Var "4506" "ih") "1" "4510") True (Var "4512" "indices")) False (Var "4520" "r")) True (Parens "4523" (App (App (App (Var "4524" "cast") True (Var "4530" "reveal")) True (Var "4538" "indices")) False (Var "4546" "r")) "4548")) True (Beta "4550" Nothing Nothing)))) (IotaProj (Var "4553" "ih") "2" "4557") Nothing "4558")) True (Var "4560" "indices")) False (Var "4568" "d")))))))))) Nothing "4570")) True (Var "4577" "d")) True (Beta "4580" Nothing Nothing))))))))) "4582",CmdDef Nothing (DefTerm "4584" "IndFixM" (Just (TpAbs "4598" True "4600" "F" (Tkk (KdArrow (Tkk (KdParens "4604" (KdArrow (Tkt (TpVar "4605" "Indices")) (KdStar "4615")) "4617")) (KdArrow (Tkt (TpVar "4620" "Indices")) (KdStar "4630")))) (TpAbs "4637" True "4639" "fm" (Tkt (TpApp (TpVar "4644" "RecFunctor") (TpVar "4657" "F"))) (TpAbs "4664" True "4666" "indices" (Tkt (TpVar "4676" "Indices")) (TpAbs "4689" False "4691" "d" (Tkt (TpAppt (TpAppt (TpApp (TpVar "4695" "FixM") (TpVar "4702" "F")) (Var "4704" "fm")) (Var "4707" "indices"))) (TpAbs "4720" True "4722" "Q" (Tkk (KdAbs "4726" "4728" "indices" (Tkt (TpVar "4738" "Indices")) (KdArrow (Tkt (TpAppt (TpAppt (TpApp (TpVar "4747" "FixM") (TpVar "4754" "F")) (Var "4756" "fm")) (Var "4759" "indices"))) (KdStar "4769")))) (TpArrow (TpParens "4776" (TpAbs "4777" True "4779" "R" (Tkk (KdArrow (Tkt (TpVar "4783" "Indices")) (KdStar "4793"))) (TpAbs "4801" True "4803" "reveal" (Tkt (TpApp (TpApp (TpVar "4812" "Cast") (TpVar "4819" "R")) (TpParens "4823" (TpAppt (TpApp (TpVar "4824" "FixM") (TpVar "4831" "F")) (Var "4833" "fm")) "4836"))) (TpArrow (TpParens "4843" (TpIota "4844" "4846" "o" (TpAbs "4850" True "4852" "indices" (Tkt (TpVar "4862" "Indices")) (TpArrow (TpAppt (TpVar "4871" "R") (Var "4873" "indices")) False (TpAppt (TpApp (TpVar "4883" "F") (TpVar "4887" "R")) (Var "4889" "indices")))) (TpEq "4898" (Var "4899" "o") (Var "4903" "outFix") "4910")) "4911") True (TpArrow (TpParens "4919" (TpAbs "4920" True "4922" "indices" (Tkt (TpVar "4932" "Indices")) (TpAbs "4941" False "4943" "r" (Tkt (TpAppt (TpVar "4947" "R") (Var "4949" "indices"))) (TpAppt (TpAppt (TpVar "4958" "Q") (Var "4960" "indices")) (Parens "4968" (App (App (App (Var "4969" "cast") True (Var "4975" "reveal")) True (Var "4983" "indices")) False (Var "4991" "r")) "4993")))) "4994") False (TpAbs "5002" True "5004" "indices" (Tkt (TpVar "5014" "Indices")) (TpAbs "5028" False "5030" "x" (Tkt (TpAppt (TpApp (TpVar "5034" "F") (TpVar "5038" "R")) (Var "5040" "indices"))) (TpAppt (TpAppt (TpVar "5054" "Q") (Var "5056" "indices")) (Parens "5064" (App (App (App (Var "5065" "inFix") True (Var "5072" "fm")) True (Var "5076" "indices")) False (Parens "5084" (App (App (App (Var "5085" "cast") True (Parens "5091" (App (Var "5092" "fm") True (Var "5096" "reveal")) "5103")) True (Var "5105" "indices")) False (Var "5113" "x")) "5115")) "5116")))))))) "5117") False (TpAppt (TpAppt (TpVar "5124" "Q") (Var "5126" "indices")) (Var "5134" "d"))))))))) (Lam "5140" True "5142" "F" Nothing (Lam "5145" True "5147" "fm" Nothing (Lam "5151" True "5153" "indices" Nothing (Lam "5162" False "5164" "d" Nothing (Lam "5167" True "5169" "Q" Nothing (Lam "5172" False "5174" "alg" Nothing (App (AppTp (App (App (App (AppTp (Var "5179" "IndFixM'") (TpVar "5190" "F")) True (Var "5193" "fm")) True (Var "5197" "indices")) False (Var "5205" "d")) (TpVar "5209" "Q")) False (IotaPair "5215" (Beta "5216" Nothing (Just (PosTerm (Var "5218" "alg") "5222"))) (Lam "5224" True "5226" "R" Nothing (Lam "5229" True "5231" "rvl" Nothing (Lam "5236" True "5238" "out" Nothing (Lam "5243" False "5245" "ih" Nothing (App (App (App (AppTp (Var "5249" "alg") (TpVar "5255" "R")) True (Var "5258" "rvl")) True (Var "5263" "out")) False (IotaProj (Var "5267" "ih") "1" "5271")))))) Nothing "5272"))))))))) "5273",CmdDef Nothing (DefTerm "5275" "lambek" (Just (TpAbs "5288" True "5290" "F" (Tkk (KdArrow (Tkk (KdParens "5294" (KdArrow (Tkt (TpVar "5295" "Indices")) (KdStar "5305")) "5307")) (KdArrow (Tkt (TpVar "5310" "Indices")) (KdStar "5320")))) (TpAbs "5327" True "5329" "fm" (Tkt (TpApp (TpVar "5334" "RecFunctor") (TpVar "5347" "F"))) (TpAbs "5354" True "5356" "indices" (Tkt (TpVar "5366" "Indices")) (TpAbs "5379" False "5381" "d" (Tkt (TpAppt (TpAppt (TpApp (TpVar "5385" "FixM") (TpVar "5392" "F")) (Var "5394" "fm")) (Var "5397" "indices"))) (TpEq "5410" (App (Var "5411" "inFix") False (Parens "5417" (App (Var "5418" "outFix") False (Var "5425" "d")) "5427")) (Var "5430" "d") "5432")))))) (Lam "5437" True "5439" "F" Nothing (Lam "5442" True "5444" "fm" Nothing (Lam "5448" True "5450" "indices" Nothing (Lam "5459" False "5461" "d" Nothing (App (AppTp (App (App (App (AppTp (Var "5464" "IndFixM") (TpVar "5474" "F")) True (Var "5477" "fm")) True (Var "5481" "indices")) False (Var "5489" "d")) (TpParens "5497" (TpLam "5498" "5500" "indices" (Tkt (TpVar "5510" "Indices")) (TpLam "5519" "5521" "d" (Tkt (TpAppt (TpAppt (TpApp (TpVar "5525" "FixM") (TpVar "5532" "F")) (Var "5534" "fm")) (Var "5537" "indices"))) (TpEq "5546" (App (Var "5547" "inFix") False (Parens "5553" (App (Var "5554" "outFix") False (Var "5561" "d")) "5563")) (Var "5566" "d") "5568"))) "5569")) False (Parens "5574" (Lam "5575" True "5577" "R" Nothing (Lam "5580" True "5582" "rvl" Nothing (Lam "5587" True "5589" "out" Nothing (Lam "5594" False "5596" "ih" Nothing (Lam "5600" True "5602" "indices" Nothing (Lam "5611" False "5613" "d" Nothing (Beta "5616" Nothing Nothing))))))) "5618"))))))) "5619"] "5619"
  