blob: 5c64716c7226bbb39e98529d6405dc97d5c2f367 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Inductive list0 : Set := nil0 : list0 | cons0 : Set -> 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.
|
