(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* list0 -> list0. Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99.