Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / StreamsLib.glob @ 6a93d814

History | View | Annotate | Download (57.9 KB)

1 6a93d814 xthirioux
DIGEST a67e786cf59f0f9bb308946312df06f5
2
FStreamsLib
3
R15:21 Coq.Lists.Streams <> <> lib
4
R32:35 Coq.Lists.List <> <> lib
5
R53:58 Coq.Setoids.Setoid <> <> lib
6
R76:95 Coq.Relations.Relation_Definitions <> <> lib
7
R113:122 Coq.Program.Wf <> <> lib
8
R140:145 Coq.Arith.Wf_nat <> <> lib
9
R163:173 Coq.Wellfounded.Wellfounded <> <> lib
10
def 188:191 <> mapT
11
R243:243 StreamsLib <> F var
12
R245:245 StreamsLib <> B var
13
R234:234 StreamsLib <> F var
14
R236:236 StreamsLib <> A var
15
R227:227 StreamsLib <> B var
16
R222:222 StreamsLib <> A var
17
def 261:266 <> applyT
18
R322:322 StreamsLib <> F var
19
R324:324 StreamsLib <> B var
20
R313:313 StreamsLib <> F var
21
R315:315 StreamsLib <> A var
22
R297:297 StreamsLib <> F var
23
R305:305 StreamsLib <> B var
24
R300:300 StreamsLib <> A var
25
def 340:351 <> option_apply
26
R362:367 StreamsLib <> applyT def
27
R378:378 StreamsLib <> B var
28
R376:376 StreamsLib <> A var
29
R369:374 Coq.Init.Datatypes <> option ind
30
R405:405 StreamsLib <> a var
31
R402:402 StreamsLib <> f var
32
R415:418 Coq.Init.Datatypes <> Some constr
33
R423:426 Coq.Init.Datatypes <> Some constr
34
R433:436 Coq.Init.Datatypes <> Some constr
35
R439:439 StreamsLib <> f var
36
R441:441 StreamsLib <> a var
37
R465:468 Coq.Init.Datatypes <> None constr
38
ax 484:490 <> eqst_eq
39
R513:518 Coq.Lists.Streams <> Stream coind
40
R520:520 StreamsLib <> A var
41
R538:540 Coq.Init.Logic <> :type_scope:x_'='_x not
42
R537:537 StreamsLib <> s var
43
R541:542 StreamsLib <> s' var
44
R524:527 Coq.Lists.Streams <> EqSt coind
45
R531:532 StreamsLib <> s' var
46
R529:529 StreamsLib <> s var
47
prf 554:560 <> inv_inv
48
R580:585 Coq.Lists.Streams <> Stream coind
49
R587:587 StreamsLib <> A var
50
R603:608 Coq.Lists.Streams <> Stream coind
51
R610:610 StreamsLib <> A var
52
R628:633 Coq.Lists.Streams <> ForAll coind
53
R659:659 StreamsLib <> s var
54
R646:651 Coq.Lists.Streams <> ForAll coind
55
R655:656 StreamsLib <> s' var
56
R653:653 StreamsLib <> P var
57
R614:619 Coq.Lists.Streams <> ForAll coind
58
R623:623 StreamsLib <> s var
59
R621:621 StreamsLib <> P var
60
R733:746 Coq.Lists.Streams <> HereAndFurther constr
61
R733:746 Coq.Lists.Streams <> HereAndFurther constr
62
prf 823:829 <> evt_inv
63
R851:856 Coq.Lists.Streams <> Stream coind
64
R858:858 StreamsLib <> A var
65
R874:879 Coq.Lists.Streams <> Stream coind
66
R881:881 StreamsLib <> A var
67
R915:920 Coq.Lists.Streams <> Exists ind
68
R947:947 StreamsLib <> s var
69
R937:940 Coq.Init.Logic <> :type_scope:x_'/\'_x not
70
R933:933 StreamsLib <> P var
71
R935:936 StreamsLib <> s' var
72
R941:941 StreamsLib <> Q var
73
R943:944 StreamsLib <> s' var
74
R901:906 Coq.Lists.Streams <> Exists ind
75
R910:910 StreamsLib <> s var
76
R908:908 StreamsLib <> Q var
77
R887:892 Coq.Lists.Streams <> ForAll coind
78
R896:896 StreamsLib <> s var
79
R894:894 StreamsLib <> P var
80
R977:980 Coq.Lists.Streams <> Here constr
81
R977:980 Coq.Lists.Streams <> Here constr
82
R0:-1 StreamsLib <> y var
83
R1017:1023 Coq.Lists.Streams <> Further constr
84
R1017:1023 Coq.Lists.Streams <> Further constr
85
def 1087:1098 <> ForAll_apply
86
R1112:1117 Coq.Lists.Streams <> Stream coind
87
R1119:1119 StreamsLib <> A var
88
R1196:1201 Coq.Lists.Streams <> ForAll coind
89
R1205:1205 StreamsLib <> s var
90
R1203:1203 StreamsLib <> Q var
91
R1160:1165 Coq.Lists.Streams <> ForAll coind
92
R1189:1189 StreamsLib <> s var
93
R1184:1184 StreamsLib <> Q var
94
R1186:1186 StreamsLib <> s var
95
R1177:1177 StreamsLib <> P var
96
R1179:1179 StreamsLib <> s var
97
R1144:1149 Coq.Lists.Streams <> ForAll coind
98
R1153:1153 StreamsLib <> s var
99
R1151:1151 StreamsLib <> P var
100
R1257:1265 StreamsLib <> always_pq var
101
R1247:1254 StreamsLib <> always_p var
102
R1276:1289 Coq.Lists.Streams <> HereAndFurther constr
103
R1308:1321 Coq.Lists.Streams <> HereAndFurther constr
104
R1343:1356 Coq.Lists.Streams <> HereAndFurther constr
105
R1372:1383 StreamsLib <> ForAll_apply def
106
R1386:1387 Coq.Lists.Streams <> tl def
107
R1389:1389 StreamsLib <> s var
108
R1358:1358 StreamsLib <> s var
109
def 1432:1444 <> necessitation
110
R1455:1460 Coq.Lists.Streams <> Stream coind
111
R1462:1462 StreamsLib <> A var
112
R1488:1488 StreamsLib <> P var
113
R1490:1490 StreamsLib <> s var
114
R1497:1502 Coq.Lists.Streams <> ForAll coind
115
R1506:1506 StreamsLib <> s var
116
R1504:1504 StreamsLib <> P var
117
R1512:1525 Coq.Lists.Streams <> HereAndFurther constr
118
R1536:1548 StreamsLib <> necessitation def
119
R1553:1554 Coq.Lists.Streams <> tl def
120
R1556:1556 StreamsLib <> s var
121
R1550:1550 StreamsLib <> I var
122
R1530:1530 StreamsLib <> I var
123
R1532:1532 StreamsLib <> s var
124
R1527:1527 StreamsLib <> s var
125
def 1573:1588 <> ForAll_reinforce
126
R1602:1607 Coq.Lists.Streams <> Stream coind
127
R1609:1609 StreamsLib <> A var
128
R1670:1675 Coq.Lists.Streams <> ForAll coind
129
R1679:1679 StreamsLib <> s var
130
R1677:1677 StreamsLib <> Q var
131
R1634:1639 Coq.Lists.Streams <> ForAll coind
132
R1663:1663 StreamsLib <> s var
133
R1654:1657 Coq.Init.Logic <> :type_scope:x_'/\'_x not
134
R1651:1651 StreamsLib <> P var
135
R1653:1653 StreamsLib <> s var
136
R1658:1658 StreamsLib <> Q var
137
R1660:1660 StreamsLib <> s var
138
R1705:1716 StreamsLib <> ForAll_apply def
139
R1705:1716 StreamsLib <> ForAll_apply def
140
R1737:1749 StreamsLib <> necessitation def
141
R1737:1749 StreamsLib <> necessitation def
142
R0:-1 StreamsLib <> y var
143
R0:-1 StreamsLib <> y var
144
def 1785:1790 <> concat
145
R1806:1809 Coq.Init.Datatypes <> list ind
146
R1811:1811 StreamsLib <> A var
147
R1824:1829 Coq.Lists.Streams <> Stream coind
148
R1831:1831 StreamsLib <> A var
149
R1836:1841 Coq.Lists.Streams <> Stream coind
150
R1843:1843 StreamsLib <> A var
151
R1849:1862 Coq.Lists.List <> fold_left def
152
R1893:1898 StreamsLib <> suffix var
153
R1886:1891 StreamsLib <> prefix var
154
R1876:1879 Coq.Lists.Streams <> Cons constr
155
R1883:1883 StreamsLib <> q var
156
R1881:1881 StreamsLib <> t var
157
prf 1910:1920 <> eqst_concat
158
R1951:1956 Coq.Lists.Streams <> Stream coind
159
R1958:1958 StreamsLib <> A var
160
R1979:1982 Coq.Lists.Streams <> EqSt coind
161
R2002:2007 StreamsLib <> concat def
162
R2013:2016 StreamsLib <> sfx' var
163
R2009:2011 StreamsLib <> pfx var
164
R1985:1990 StreamsLib <> concat def
165
R1996:1998 StreamsLib <> sfx var
166
R1992:1994 StreamsLib <> pfx var
167
R1962:1965 Coq.Lists.Streams <> EqSt coind
168
R1971:1974 StreamsLib <> sfx' var
169
R1967:1969 StreamsLib <> sfx var
170
R2088:2091 Coq.Lists.Streams <> eqst constr
171
R2088:2091 Coq.Lists.Streams <> eqst constr
172
prf 2135:2145 <> concat_eqst
173
R2181:2186 Coq.Lists.Streams <> Stream coind
174
R2188:2188 StreamsLib <> A var
175
R2284:2287 Coq.Init.Logic <> :type_scope:x_'/\'_x not
176
R2277:2279 Coq.Init.Logic <> :type_scope:x_'='_x not
177
R2274:2276 StreamsLib <> pfx var
178
R2280:2283 StreamsLib <> pfx' var
179
R2288:2291 Coq.Lists.Streams <> EqSt coind
180
R2297:2300 StreamsLib <> sfx' var
181
R2293:2295 StreamsLib <> sfx var
182
R2230:2233 Coq.Lists.Streams <> EqSt coind
183
R2253:2258 StreamsLib <> concat def
184
R2265:2268 StreamsLib <> sfx' var
185
R2260:2263 StreamsLib <> pfx' var
186
R2236:2241 StreamsLib <> concat def
187
R2247:2249 StreamsLib <> sfx var
188
R2243:2245 StreamsLib <> pfx var
189
R2207:2209 Coq.Init.Logic <> :type_scope:x_'='_x not
190
R2192:2202 Coq.Lists.List <> length syndef
191
R2204:2206 StreamsLib <> pfx var
192
R2210:2220 Coq.Lists.List <> length syndef
193
R2222:2225 StreamsLib <> pfx' var
194
R0:-1 StreamsLib <> y var
195
R0:-1 StreamsLib <> y var
196
R0:-1 StreamsLib <> y var
197
R0:-1 StreamsLib <> y var
198
prf 2588:2593 <> evt_id
199
R2613:2618 Coq.Lists.Streams <> Stream coind
200
R2620:2620 StreamsLib <> A var
201
R2624:2629 Coq.Lists.Streams <> Exists ind
202
R2650:2650 StreamsLib <> s var
203
R2643:2645 Coq.Init.Logic <> :type_scope:x_'='_x not
204
R2642:2642 StreamsLib <> s var
205
R2646:2647 StreamsLib <> s' var
206
R2674:2677 Coq.Lists.Streams <> Here constr
207
R2674:2677 Coq.Lists.Streams <> Here constr
208
prf 2707:2716 <> evt_concat
209
R2736:2741 Coq.Lists.Streams <> Stream coind
210
R2743:2743 StreamsLib <> A var
211
R2761:2766 Coq.Lists.Streams <> Stream coind
212
R2768:2768 StreamsLib <> A var
213
R2786:2791 Coq.Lists.Streams <> Exists ind
214
R2796:2801 StreamsLib <> concat def
215
R2805:2805 StreamsLib <> s var
216
R2803:2803 StreamsLib <> p var
217
R2793:2793 StreamsLib <> P var
218
R2772:2777 Coq.Lists.Streams <> Exists ind
219
R2781:2781 StreamsLib <> s var
220
R2779:2779 StreamsLib <> P var
221
R2866:2869 Coq.Lists.Streams <> Cons constr
222
R2866:2869 Coq.Lists.Streams <> Cons constr
223
R2885:2891 Coq.Lists.Streams <> Further constr
224
R2885:2891 Coq.Lists.Streams <> Further constr
225
prf 2918:2927 <> inv_concat
226
R2947:2952 Coq.Lists.Streams <> Stream coind
227
R2954:2954 StreamsLib <> A var
228
R2972:2977 Coq.Lists.Streams <> Stream coind
229
R2979:2979 StreamsLib <> A var
230
R3008:3013 Coq.Lists.Streams <> ForAll coind
231
R3017:3017 StreamsLib <> s var
232
R3015:3015 StreamsLib <> P var
233
R2983:2988 Coq.Lists.Streams <> ForAll coind
234
R2993:2998 StreamsLib <> concat def
235
R3002:3002 StreamsLib <> s var
236
R3000:3000 StreamsLib <> p var
237
R2990:2990 StreamsLib <> P var
238
R3090:3093 Coq.Lists.Streams <> Cons constr
239
R3090:3093 Coq.Lists.Streams <> Cons constr
240
def 3160:3163 <> lift
241
R3174:3174 StreamsLib <> A var
242
R3180:3183 Coq.Lists.Streams <> Cons constr
243
R3188:3191 StreamsLib <> lift def
244
R3193:3193 StreamsLib <> v var
245
R3185:3185 StreamsLib <> v var
246
prf 3204:3210 <> hd_lift
247
R3230:3230 StreamsLib <> A var
248
R3245:3247 Coq.Init.Logic <> :type_scope:x_'='_x not
249
R3234:3235 Coq.Lists.Streams <> hd def
250
R3238:3241 StreamsLib <> lift def
251
R3243:3243 StreamsLib <> v var
252
R3248:3248 StreamsLib <> v var
253
prf 3283:3289 <> tl_lift
254
R3309:3309 StreamsLib <> A var
255
R3324:3326 Coq.Init.Logic <> :type_scope:x_'='_x not
256
R3313:3314 Coq.Lists.Streams <> tl def
257
R3317:3320 StreamsLib <> lift def
258
R3322:3322 StreamsLib <> v var
259
R3327:3330 StreamsLib <> lift def
260
R3332:3332 StreamsLib <> v var
261
def 3372:3376 <> apply
262
R3387:3392 StreamsLib <> applyT def
263
R3403:3403 StreamsLib <> B var
264
R3401:3401 StreamsLib <> A var
265
R3394:3399 Coq.Lists.Streams <> Stream coind
266
R3430:3430 StreamsLib <> a var
267
R3427:3427 StreamsLib <> f var
268
R3441:3444 Coq.Lists.Streams <> Cons constr
269
R3455:3458 Coq.Lists.Streams <> Cons constr
270
R3470:3473 Coq.Lists.Streams <> Cons constr
271
R3484:3488 StreamsLib <> apply def
272
prf 3510:3517 <> hd_apply
273
R3539:3544 Coq.Lists.Streams <> Stream coind
274
R3552:3552 StreamsLib <> B var
275
R3547:3547 StreamsLib <> A var
276
R3561:3566 Coq.Lists.Streams <> Stream coind
277
R3568:3568 StreamsLib <> A var
278
R3586:3588 Coq.Init.Logic <> :type_scope:x_'='_x not
279
R3572:3573 Coq.Lists.Streams <> hd def
280
R3576:3580 StreamsLib <> apply def
281
R3584:3584 StreamsLib <> a var
282
R3582:3582 StreamsLib <> f var
283
R3590:3591 Coq.Lists.Streams <> hd def
284
R3593:3593 StreamsLib <> f var
285
R3597:3598 Coq.Lists.Streams <> hd def
286
R3600:3600 StreamsLib <> a var
287
prf 3660:3667 <> tl_apply
288
R3689:3694 Coq.Lists.Streams <> Stream coind
289
R3702:3702 StreamsLib <> B var
290
R3697:3697 StreamsLib <> A var
291
R3711:3716 Coq.Lists.Streams <> Stream coind
292
R3718:3718 StreamsLib <> A var
293
R3736:3738 Coq.Init.Logic <> :type_scope:x_'='_x not
294
R3722:3723 Coq.Lists.Streams <> tl def
295
R3726:3730 StreamsLib <> apply def
296
R3734:3734 StreamsLib <> a var
297
R3732:3732 StreamsLib <> f var
298
R3739:3743 StreamsLib <> apply def
299
R3753:3754 Coq.Lists.Streams <> tl def
300
R3756:3756 StreamsLib <> a var
301
R3746:3747 Coq.Lists.Streams <> tl def
302
R3749:3749 StreamsLib <> f var
303
prf 3816:3825 <> cons_apply
304
R3853:3853 StreamsLib <> B var
305
R3848:3848 StreamsLib <> A var
306
R3862:3867 Coq.Lists.Streams <> Stream coind
307
R3875:3875 StreamsLib <> B var
308
R3870:3870 StreamsLib <> A var
309
R3885:3885 StreamsLib <> A var
310
R3894:3899 Coq.Lists.Streams <> Stream coind
311
R3901:3901 StreamsLib <> A var
312
R3905:3908 Coq.Lists.Streams <> EqSt coind
313
R3945:3948 Coq.Lists.Streams <> Cons constr
314
R3959:3963 StreamsLib <> apply def
315
R3968:3969 StreamsLib <> a' var
316
R3965:3966 StreamsLib <> f' var
317
R3951:3952 StreamsLib <> f0 var
318
R3954:3955 StreamsLib <> a0 var
319
R3911:3915 StreamsLib <> apply def
320
R3931:3934 Coq.Lists.Streams <> Cons constr
321
R3939:3940 StreamsLib <> a' var
322
R3936:3937 StreamsLib <> a0 var
323
R3918:3921 Coq.Lists.Streams <> Cons constr
324
R3926:3927 StreamsLib <> f' var
325
R3923:3924 StreamsLib <> f0 var
326
R3995:3998 Coq.Lists.Streams <> eqst constr
327
R3995:3998 Coq.Lists.Streams <> eqst constr
328
R4023:4033 Coq.Lists.Streams <> EqSt_reflex thm
329
R4023:4033 Coq.Lists.Streams <> EqSt_reflex thm
330
prf 4048:4057 <> eqst_apply
331
R4082:4087 Coq.Lists.Streams <> Stream coind
332
R4095:4095 StreamsLib <> B var
333
R4090:4090 StreamsLib <> A var
334
R4107:4112 Coq.Lists.Streams <> Stream coind
335
R4114:4114 StreamsLib <> A var
336
R4146:4149 Coq.Lists.Streams <> EqSt coind
337
R4164:4168 StreamsLib <> apply def
338
R4173:4174 StreamsLib <> a' var
339
R4170:4171 StreamsLib <> f' var
340
R4152:4156 StreamsLib <> apply def
341
R4160:4160 StreamsLib <> a var
342
R4158:4158 StreamsLib <> f var
343
R4133:4136 Coq.Lists.Streams <> EqSt coind
344
R4140:4141 StreamsLib <> a' var
345
R4138:4138 StreamsLib <> a var
346
R4120:4123 Coq.Lists.Streams <> EqSt coind
347
R4127:4128 StreamsLib <> f' var
348
R4125:4125 StreamsLib <> f var
349
R4251:4254 Coq.Lists.Streams <> eqst constr
350
R4251:4254 Coq.Lists.Streams <> eqst constr
351
R4266:4273 StreamsLib <> hd_apply thm
352
R4266:4273 StreamsLib <> hd_apply thm
353
R4285:4292 StreamsLib <> hd_apply thm
354
R4285:4292 StreamsLib <> hd_apply thm
355
R4318:4325 StreamsLib <> tl_apply thm
356
R4318:4325 StreamsLib <> tl_apply thm
357
R4337:4344 StreamsLib <> tl_apply thm
358
R4337:4344 StreamsLib <> tl_apply thm
359
prf 4404:4410 <> inv_map
360
R4437:4437 StreamsLib <> B var
361
R4432:4432 StreamsLib <> A var
362
R4447:4452 Coq.Lists.Streams <> Stream coind
363
R4454:4454 StreamsLib <> A var
364
R4489:4494 Coq.Lists.Streams <> ForAll coind
365
R4530:4530 StreamsLib <> s var
366
R4507:4507 StreamsLib <> P var
367
R4510:4514 StreamsLib <> apply def
368
R4525:4526 StreamsLib <> s' var
369
R4517:4520 StreamsLib <> lift def
370
R4522:4522 StreamsLib <> f var
371
R4458:4463 Coq.Lists.Streams <> ForAll coind
372
R4468:4472 StreamsLib <> apply def
373
R4483:4483 StreamsLib <> s var
374
R4475:4478 StreamsLib <> lift def
375
R4480:4480 StreamsLib <> f var
376
R4465:4465 StreamsLib <> P var
377
R4621:4634 Coq.Lists.Streams <> HereAndFurther constr
378
R4621:4634 Coq.Lists.Streams <> HereAndFurther constr
379
prf 4700:4706 <> map_inv
380
R4733:4733 StreamsLib <> B var
381
R4728:4728 StreamsLib <> A var
382
R4743:4748 Coq.Lists.Streams <> Stream coind
383
R4750:4750 StreamsLib <> A var
384
R4800:4805 Coq.Lists.Streams <> ForAll coind
385
R4810:4814 StreamsLib <> apply def
386
R4825:4825 StreamsLib <> s var
387
R4817:4820 StreamsLib <> lift def
388
R4822:4822 StreamsLib <> f var
389
R4807:4807 StreamsLib <> P var
390
R4754:4759 Coq.Lists.Streams <> ForAll coind
391
R4795:4795 StreamsLib <> s var
392
R4772:4772 StreamsLib <> P var
393
R4775:4779 StreamsLib <> apply def
394
R4790:4791 StreamsLib <> s' var
395
R4782:4785 StreamsLib <> lift def
396
R4787:4787 StreamsLib <> f var
397
R4917:4930 Coq.Lists.Streams <> HereAndFurther constr
398
R4917:4930 Coq.Lists.Streams <> HereAndFurther constr
399
prf 4996:5002 <> evt_map
400
R5029:5029 StreamsLib <> B var
401
R5024:5024 StreamsLib <> A var
402
R5039:5044 Coq.Lists.Streams <> Stream coind
403
R5046:5046 StreamsLib <> A var
404
R5081:5086 Coq.Lists.Streams <> Exists ind
405
R5122:5122 StreamsLib <> s var
406
R5099:5099 StreamsLib <> P var
407
R5102:5106 StreamsLib <> apply def
408
R5117:5118 StreamsLib <> s' var
409
R5109:5112 StreamsLib <> lift def
410
R5114:5114 StreamsLib <> f var
411
R5050:5055 Coq.Lists.Streams <> Exists ind
412
R5060:5064 StreamsLib <> apply def
413
R5075:5075 StreamsLib <> s var
414
R5067:5070 StreamsLib <> lift def
415
R5072:5072 StreamsLib <> f var
416
R5057:5057 StreamsLib <> P var
417
R5160:5164 StreamsLib <> apply def
418
R5167:5170 StreamsLib <> lift def
419
R5160:5164 StreamsLib <> apply def
420
R5167:5170 StreamsLib <> lift def
421
R5239:5242 Coq.Lists.Streams <> Here constr
422
R5239:5242 Coq.Lists.Streams <> Here constr
423
R5291:5297 Coq.Lists.Streams <> Further constr
424
R5291:5297 Coq.Lists.Streams <> Further constr
425
R5318:5319 Coq.Lists.Streams <> tl def
426
R5318:5319 Coq.Lists.Streams <> tl def
427
R5338:5344 StreamsLib <> tl_lift thm
428
R5338:5344 StreamsLib <> tl_lift thm
429
R5359:5366 StreamsLib <> tl_apply thm
430
R5359:5366 StreamsLib <> tl_apply thm
431
R5376:5382 Coq.Init.Logic <> f_equal thm
432
R5376:5382 Coq.Init.Logic <> f_equal thm
433
prf 5413:5419 <> map_evt
434
R5446:5446 StreamsLib <> B var
435
R5441:5441 StreamsLib <> A var
436
R5456:5461 Coq.Lists.Streams <> Stream coind
437
R5463:5463 StreamsLib <> A var
438
R5513:5518 Coq.Lists.Streams <> Exists ind
439
R5523:5527 StreamsLib <> apply def
440
R5538:5538 StreamsLib <> s var
441
R5530:5533 StreamsLib <> lift def
442
R5535:5535 StreamsLib <> f var
443
R5520:5520 StreamsLib <> P var
444
R5467:5472 Coq.Lists.Streams <> Exists ind
445
R5508:5508 StreamsLib <> s var
446
R5485:5485 StreamsLib <> P var
447
R5488:5492 StreamsLib <> apply def
448
R5503:5504 StreamsLib <> s' var
449
R5495:5498 StreamsLib <> lift def
450
R5500:5500 StreamsLib <> f var
451
R5596:5599 Coq.Lists.Streams <> Here constr
452
R5596:5599 Coq.Lists.Streams <> Here constr
453
R5620:5626 Coq.Lists.Streams <> Further constr
454
R5620:5626 Coq.Lists.Streams <> Further constr
455
R5638:5645 StreamsLib <> tl_apply thm
456
R5638:5645 StreamsLib <> tl_apply thm
457
R5657:5663 StreamsLib <> tl_lift thm
458
R5657:5663 StreamsLib <> tl_lift thm
459
def 5700:5702 <> zip
460
R5723:5725 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
461
R5715:5720 Coq.Lists.Streams <> Stream coind
462
R5722:5722 StreamsLib <> A var
463
R5726:5731 Coq.Lists.Streams <> Stream coind
464
R5733:5733 StreamsLib <> B var
465
R5739:5743 StreamsLib <> apply def
466
R5789:5791 Coq.Init.Datatypes <> snd def
467
R5793:5793 StreamsLib <> s var
468
R5746:5750 StreamsLib <> apply def
469
R5780:5782 Coq.Init.Datatypes <> fst def
470
R5784:5784 StreamsLib <> s var
471
R5753:5756 StreamsLib <> lift def
472
R5770:5770 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
473
R5772:5773 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
474
R5775:5775 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
475
R5771:5771 StreamsLib <> a var
476
R5774:5774 StreamsLib <> b var
477
prf 5804:5815 <> zip_fst_eqst
478
R5850:5855 Coq.Lists.Streams <> Stream coind
479
R5857:5857 StreamsLib <> A var
480
R5870:5875 Coq.Lists.Streams <> Stream coind
481
R5877:5877 StreamsLib <> B var
482
R5923:5926 Coq.Lists.Streams <> EqSt coind
483
R5931:5933 StreamsLib <> s1' var
484
R5928:5929 StreamsLib <> s1 var
485
R5883:5886 Coq.Lists.Streams <> EqSt coind
486
R5904:5906 StreamsLib <> zip def
487
R5908:5908 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
488
R5912:5913 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
489
R5917:5917 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
490
R5909:5911 StreamsLib <> s1' var
491
R5914:5916 StreamsLib <> s2' var
492
R5889:5891 StreamsLib <> zip def
493
R5893:5893 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
494
R5896:5897 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
495
R5900:5900 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
496
R5894:5895 StreamsLib <> s1 var
497
R5898:5899 StreamsLib <> s2 var
498
R6048:6051 Coq.Lists.Streams <> eqst constr
499
R6048:6051 Coq.Lists.Streams <> eqst constr
500
prf 6167:6173 <> zip_fst
501
R6208:6213 Coq.Lists.Streams <> Stream coind
502
R6215:6215 StreamsLib <> A var
503
R6228:6233 Coq.Lists.Streams <> Stream coind
504
R6235:6235 StreamsLib <> B var
505
R6276:6278 Coq.Init.Logic <> :type_scope:x_'='_x not
506
R6274:6275 StreamsLib <> s1 var
507
R6279:6281 StreamsLib <> s1' var
508
R6253:6255 Coq.Init.Logic <> :type_scope:x_'='_x not
509
R6241:6243 StreamsLib <> zip def
510
R6245:6245 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
511
R6248:6249 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
512
R6252:6252 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
513
R6246:6247 StreamsLib <> s1 var
514
R6250:6251 StreamsLib <> s2 var
515
R6256:6258 StreamsLib <> zip def
516
R6260:6260 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
517
R6264:6265 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
518
R6269:6269 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
519
R6261:6263 StreamsLib <> s1' var
520
R6266:6268 StreamsLib <> s2' var
521
R6305:6311 StreamsLib <> eqst_eq prfax
522
R6305:6311 StreamsLib <> eqst_eq prfax
523
R6321:6332 StreamsLib <> zip_fst_eqst thm
524
R6321:6332 StreamsLib <> zip_fst_eqst thm
525
R6367:6377 Coq.Lists.Streams <> EqSt_reflex thm
526
R6367:6377 Coq.Lists.Streams <> EqSt_reflex thm
527
prf 6392:6403 <> zip_snd_eqst
528
R6438:6443 Coq.Lists.Streams <> Stream coind
529
R6445:6445 StreamsLib <> A var
530
R6458:6463 Coq.Lists.Streams <> Stream coind
531
R6465:6465 StreamsLib <> B var
532
R6511:6514 Coq.Lists.Streams <> EqSt coind
533
R6519:6521 StreamsLib <> s2' var
534
R6516:6517 StreamsLib <> s2 var
535
R6471:6474 Coq.Lists.Streams <> EqSt coind
536
R6492:6494 StreamsLib <> zip def
537
R6496:6496 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
538
R6500:6501 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
539
R6505:6505 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
540
R6497:6499 StreamsLib <> s1' var
541
R6502:6504 StreamsLib <> s2' var
542
R6477:6479 StreamsLib <> zip def
543
R6481:6481 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
544
R6484:6485 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
545
R6488:6488 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
546
R6482:6483 StreamsLib <> s1 var
547
R6486:6487 StreamsLib <> s2 var
548
R6636:6639 Coq.Lists.Streams <> eqst constr
549
R6636:6639 Coq.Lists.Streams <> eqst constr
550
prf 6755:6761 <> zip_snd
551
R6796:6801 Coq.Lists.Streams <> Stream coind
552
R6803:6803 StreamsLib <> A var
553
R6816:6821 Coq.Lists.Streams <> Stream coind
554
R6823:6823 StreamsLib <> B var
555
R6864:6866 Coq.Init.Logic <> :type_scope:x_'='_x not
556
R6862:6863 StreamsLib <> s2 var
557
R6867:6869 StreamsLib <> s2' var
558
R6841:6843 Coq.Init.Logic <> :type_scope:x_'='_x not
559
R6829:6831 StreamsLib <> zip def
560
R6833:6833 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
561
R6836:6837 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
562
R6840:6840 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
563
R6834:6835 StreamsLib <> s1 var
564
R6838:6839 StreamsLib <> s2 var
565
R6844:6846 StreamsLib <> zip def
566
R6848:6848 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
567
R6852:6853 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
568
R6857:6857 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
569
R6849:6851 StreamsLib <> s1' var
570
R6854:6856 StreamsLib <> s2' var
571
R6893:6899 StreamsLib <> eqst_eq prfax
572
R6893:6899 StreamsLib <> eqst_eq prfax
573
R6909:6920 StreamsLib <> zip_snd_eqst thm
574
R6909:6920 StreamsLib <> zip_snd_eqst thm
575
R6955:6965 Coq.Lists.Streams <> EqSt_reflex thm
576
R6955:6965 Coq.Lists.Streams <> EqSt_reflex thm
577
def 6985:6989 <> unzip
578
R7002:7007 Coq.Lists.Streams <> Stream coind
579
R7011:7011 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
580
R7010:7010 StreamsLib <> A var
581
R7012:7012 StreamsLib <> B var
582
R7019:7019 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
583
R7045:7046 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
584
R7072:7072 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
585
R7020:7024 StreamsLib <> apply def
586
R7044:7044 StreamsLib <> s var
587
R7027:7030 StreamsLib <> lift def
588
R7034:7036 Coq.Init.Datatypes <> fst def
589
R7047:7051 StreamsLib <> apply def
590
R7071:7071 StreamsLib <> s var
591
R7054:7057 StreamsLib <> lift def
592
R7061:7063 Coq.Init.Datatypes <> snd def
593
prf 7082:7093 <> fst_zip_eqst
594
R7116:7121 Coq.Lists.Streams <> Stream coind
595
R7123:7123 StreamsLib <> A var
596
R7132:7137 Coq.Lists.Streams <> Stream coind
597
R7139:7139 StreamsLib <> B var
598
R7143:7146 Coq.Lists.Streams <> EqSt coind
599
R7189:7190 StreamsLib <> s1 var
600
R7149:7153 StreamsLib <> apply def
601
R7174:7176 StreamsLib <> zip def
602
R7178:7178 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
603
R7181:7182 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
604
R7185:7185 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
605
R7179:7180 StreamsLib <> s1 var
606
R7183:7184 StreamsLib <> s2 var
607
R7156:7159 StreamsLib <> lift def
608
R7163:7165 Coq.Init.Datatypes <> fst def
609
R7257:7260 Coq.Lists.Streams <> eqst constr
610
R7257:7260 Coq.Lists.Streams <> eqst constr
611
prf 7304:7310 <> fst_zip
612
R7333:7338 Coq.Lists.Streams <> Stream coind
613
R7340:7340 StreamsLib <> A var
614
R7349:7354 Coq.Lists.Streams <> Stream coind
615
R7356:7356 StreamsLib <> B var
616
R7398:7400 Coq.Init.Logic <> :type_scope:x_'='_x not
617
R7360:7364 StreamsLib <> apply def
618
R7385:7387 StreamsLib <> zip def
619
R7389:7389 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
620
R7392:7393 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
621
R7396:7396 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
622
R7390:7391 StreamsLib <> s1 var
623
R7394:7395 StreamsLib <> s2 var
624
R7367:7370 StreamsLib <> lift def
625
R7374:7376 Coq.Init.Datatypes <> fst def
626
R7401:7402 StreamsLib <> s1 var
627
R7426:7432 StreamsLib <> eqst_eq prfax
628
R7426:7432 StreamsLib <> eqst_eq prfax
629
R7441:7452 StreamsLib <> fst_zip_eqst thm
630
R7441:7452 StreamsLib <> fst_zip_eqst thm
631
prf 7467:7478 <> snd_zip_eqst
632
R7501:7506 Coq.Lists.Streams <> Stream coind
633
R7508:7508 StreamsLib <> A var
634
R7517:7522 Coq.Lists.Streams <> Stream coind
635
R7524:7524 StreamsLib <> B var
636
R7528:7531 Coq.Lists.Streams <> EqSt coind
637
R7574:7575 StreamsLib <> s2 var
638
R7534:7538 StreamsLib <> apply def
639
R7559:7561 StreamsLib <> zip def
640
R7563:7563 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
641
R7566:7567 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
642
R7570:7570 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
643
R7564:7565 StreamsLib <> s1 var
644
R7568:7569 StreamsLib <> s2 var
645
R7541:7544 StreamsLib <> lift def
646
R7548:7550 Coq.Init.Datatypes <> snd def
647
R7642:7645 Coq.Lists.Streams <> eqst constr
648
R7642:7645 Coq.Lists.Streams <> eqst constr
649
prf 7689:7695 <> snd_zip
650
R7718:7723 Coq.Lists.Streams <> Stream coind
651
R7725:7725 StreamsLib <> A var
652
R7734:7739 Coq.Lists.Streams <> Stream coind
653
R7741:7741 StreamsLib <> B var
654
R7783:7785 Coq.Init.Logic <> :type_scope:x_'='_x not
655
R7745:7749 StreamsLib <> apply def
656
R7770:7772 StreamsLib <> zip def
657
R7774:7774 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
658
R7777:7778 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
659
R7781:7781 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
660
R7775:7776 StreamsLib <> s1 var
661
R7779:7780 StreamsLib <> s2 var
662
R7752:7755 StreamsLib <> lift def
663
R7759:7761 Coq.Init.Datatypes <> snd def
664
R7786:7787 StreamsLib <> s2 var
665
R7811:7817 StreamsLib <> eqst_eq prfax
666
R7811:7817 StreamsLib <> eqst_eq prfax
667
R7826:7837 StreamsLib <> snd_zip_eqst thm
668
R7826:7837 StreamsLib <> snd_zip_eqst thm
669
prf 7852:7865 <> zip_unzip_eqst
670
R7887:7892 Coq.Lists.Streams <> Stream coind
671
R7896:7896 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
672
R7895:7895 StreamsLib <> A var
673
R7897:7897 StreamsLib <> B var
674
R7902:7905 Coq.Lists.Streams <> EqSt coind
675
R7923:7923 StreamsLib <> s var
676
R7908:7910 StreamsLib <> zip def
677
R7913:7917 StreamsLib <> unzip def
678
R7919:7919 StreamsLib <> s var
679
R7976:7979 Coq.Lists.Streams <> eqst constr
680
R7976:7979 Coq.Lists.Streams <> eqst constr
681
prf 8052:8060 <> zip_unzip
682
R8082:8087 Coq.Lists.Streams <> Stream coind
683
R8091:8091 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
684
R8090:8090 StreamsLib <> A var
685
R8092:8092 StreamsLib <> B var
686
R8110:8112 Coq.Init.Logic <> :type_scope:x_'='_x not
687
R8097:8099 StreamsLib <> zip def
688
R8102:8106 StreamsLib <> unzip def
689
R8108:8108 StreamsLib <> s var
690
R8113:8113 StreamsLib <> s var
691
R8137:8143 StreamsLib <> eqst_eq prfax
692
R8137:8143 StreamsLib <> eqst_eq prfax
693
R8152:8165 StreamsLib <> zip_unzip_eqst thm
694
R8152:8165 StreamsLib <> zip_unzip_eqst thm
695
prf 8182:8192 <> inv_eq_eqst
696
R8215:8220 Coq.Lists.Streams <> Stream coind
697
R8222:8222 StreamsLib <> A var
698
R8292:8295 Coq.Lists.Streams <> EqSt coind
699
R8299:8300 StreamsLib <> s' var
700
R8297:8297 StreamsLib <> s var
701
R8227:8232 Coq.Lists.Streams <> ForAll coind
702
R8276:8278 StreamsLib <> zip def
703
R8280:8280 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
704
R8282:8283 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
705
R8286:8286 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
706
R8281:8281 StreamsLib <> s var
707
R8284:8285 StreamsLib <> s' var
708
R8258:8260 Coq.Init.Logic <> :type_scope:x_'='_x not
709
R8246:8248 Coq.Init.Datatypes <> fst def
710
R8251:8252 Coq.Lists.Streams <> hd def
711
R8254:8256 StreamsLib <> ss' var
712
R8261:8263 Coq.Init.Datatypes <> snd def
713
R8266:8267 Coq.Lists.Streams <> hd def
714
R8269:8271 StreamsLib <> ss' var
715
R8408:8411 Coq.Lists.Streams <> eqst constr
716
R8408:8411 Coq.Lists.Streams <> eqst constr
717
prf 8469:8479 <> eqst_inv_eq
718
R8502:8507 Coq.Lists.Streams <> Stream coind
719
R8509:8509 StreamsLib <> A var
720
R8528:8533 Coq.Lists.Streams <> ForAll coind
721
R8577:8579 StreamsLib <> zip def
722
R8581:8581 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
723
R8583:8584 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
724
R8587:8587 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
725
R8582:8582 StreamsLib <> s var
726
R8585:8586 StreamsLib <> s' var
727
R8559:8561 Coq.Init.Logic <> :type_scope:x_'='_x not
728
R8547:8549 Coq.Init.Datatypes <> fst def
729
R8552:8553 Coq.Lists.Streams <> hd def
730
R8555:8557 StreamsLib <> ss' var
731
R8562:8564 Coq.Init.Datatypes <> snd def
732
R8567:8568 Coq.Lists.Streams <> hd def
733
R8570:8572 StreamsLib <> ss' var
734
R8515:8518 Coq.Lists.Streams <> EqSt coind
735
R8522:8523 StreamsLib <> s' var
736
R8520:8520 StreamsLib <> s var
737
R8696:8709 Coq.Lists.Streams <> HereAndFurther constr
738
R8696:8709 Coq.Lists.Streams <> HereAndFurther constr
739
def 8771:8781 <> history_rec
740
R8795:8798 Coq.Init.Datatypes <> list ind
741
R8800:8800 StreamsLib <> A var
742
R8808:8813 Coq.Lists.Streams <> Stream coind
743
R8815:8815 StreamsLib <> A var
744
R8820:8825 Coq.Lists.Streams <> Stream coind
745
R8834:8836 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
746
R8828:8831 Coq.Init.Datatypes <> list ind
747
R8833:8833 StreamsLib <> A var
748
R8837:8837 StreamsLib <> A var
749
R8850:8850 StreamsLib <> s var
750
R8860:8863 Coq.Lists.Streams <> Cons constr
751
R8874:8877 Coq.Lists.Streams <> Cons constr
752
R8891:8901 StreamsLib <> history_rec def
753
R8904:8907 Coq.Init.Datatypes <> cons constr
754
R8912:8915 StreamsLib <> past var
755
R8879:8879 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
756
R8884:8885 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
757
R8888:8888 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
758
R8880:8883 StreamsLib <> past var
759
def 8940:8946 <> history
760
R8957:8962 Coq.Lists.Streams <> Stream coind
761
R8964:8964 StreamsLib <> A var
762
R8969:8974 Coq.Lists.Streams <> Stream coind
763
R8983:8985 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
764
R8977:8980 Coq.Init.Datatypes <> list ind
765
R8982:8982 StreamsLib <> A var
766
R8986:8986 StreamsLib <> A var
767
R8992:9002 StreamsLib <> history_rec def
768
R9008:9008 StreamsLib <> s var
769
R9004:9006 Coq.Init.Datatypes <> nil constr
770
prf 9021:9036 <> eqst_history_rec
771
R9058:9061 Coq.Init.Datatypes <> list ind
772
R9063:9063 StreamsLib <> A var
773
R9078:9083 Coq.Lists.Streams <> Stream coind
774
R9085:9085 StreamsLib <> A var
775
R9108:9111 Coq.Lists.Streams <> EqSt coind
776
R9136:9146 StreamsLib <> history_rec def
777
R9152:9155 StreamsLib <> sfx' var
778
R9148:9150 StreamsLib <> pfx var
779
R9114:9124 StreamsLib <> history_rec def
780
R9130:9132 StreamsLib <> sfx var
781
R9126:9128 StreamsLib <> pfx var
782
R9091:9094 Coq.Lists.Streams <> EqSt coind
783
R9100:9103 StreamsLib <> sfx' var
784
R9096:9098 StreamsLib <> sfx var
785
R9305:9308 Coq.Lists.Streams <> eqst constr
786
R9305:9308 Coq.Lists.Streams <> eqst constr
787
prf 9382:9393 <> eqst_history
788
R9420:9425 Coq.Lists.Streams <> Stream coind
789
R9427:9427 StreamsLib <> A var
790
R9450:9453 Coq.Lists.Streams <> EqSt coind
791
R9470:9476 StreamsLib <> history def
792
R9478:9481 StreamsLib <> sfx' var
793
R9456:9462 StreamsLib <> history def
794
R9464:9466 StreamsLib <> sfx var
795
R9433:9436 Coq.Lists.Streams <> EqSt coind
796
R9442:9445 StreamsLib <> sfx' var
797
R9438:9440 StreamsLib <> sfx var
798
R9506:9521 StreamsLib <> eqst_history_rec thm
799
R9506:9521 StreamsLib <> eqst_history_rec thm
800
prf 9550:9566 <> unzip_history_rec
801
R9588:9591 Coq.Init.Datatypes <> list ind
802
R9593:9593 StreamsLib <> A var
803
R9603:9608 Coq.Lists.Streams <> Stream coind
804
R9610:9610 StreamsLib <> A var
805
R9614:9617 Coq.Lists.Streams <> EqSt coind
806
R9655:9657 StreamsLib <> sfx var
807
R9620:9622 Coq.Init.Datatypes <> snd def
808
R9625:9629 StreamsLib <> unzip def
809
R9632:9642 StreamsLib <> history_rec def
810
R9648:9650 StreamsLib <> sfx var
811
R9644:9646 StreamsLib <> pfx var
812
R9725:9728 Coq.Lists.Streams <> eqst constr
813
R9725:9728 Coq.Lists.Streams <> eqst constr
814
prf 9774:9786 <> unzip_history
815
R9806:9811 Coq.Lists.Streams <> Stream coind
816
R9813:9813 StreamsLib <> A var
817
R9817:9820 Coq.Lists.Streams <> EqSt coind
818
R9848:9848 StreamsLib <> s var
819
R9823:9825 Coq.Init.Datatypes <> snd def
820
R9828:9832 StreamsLib <> unzip def
821
R9835:9841 StreamsLib <> history def
822
R9843:9843 StreamsLib <> s var
823
R9865:9871 StreamsLib <> history def
824
R9888:9904 StreamsLib <> unzip_history_rec thm
825
R9888:9904 StreamsLib <> unzip_history_rec thm
826
def 9924:9935 <> History_Spec
827
R9946:9951 Coq.Lists.Streams <> Stream coind
828
R9953:9953 StreamsLib <> A var
829
R10018:10023 Coq.Init.Logic <> :type_scope:x_'/\'_x not
830
R9983:9985 Coq.Init.Logic <> :type_scope:x_'='_x not
831
R9967:9969 Coq.Init.Datatypes <> fst def
832
R9972:9973 Coq.Lists.Streams <> hd def
833
R9976:9977 Coq.Lists.Streams <> tl def
834
R9979:9980 StreamsLib <> s' var
835
R9986:9989 Coq.Init.Datatypes <> cons constr
836
R10006:10008 Coq.Init.Datatypes <> fst def
837
R10011:10012 Coq.Lists.Streams <> hd def
838
R10014:10015 StreamsLib <> s' var
839
R9992:9994 Coq.Init.Datatypes <> snd def
840
R9997:9998 Coq.Lists.Streams <> hd def
841
R10000:10001 StreamsLib <> s' var
842
R10024:10027 Coq.Lists.Streams <> EqSt coind
843
R10081:10081 StreamsLib <> s var
844
R10030:10035 StreamsLib <> concat def
845
R10052:10056 StreamsLib <> apply def
846
R10076:10077 StreamsLib <> s' var
847
R10059:10062 StreamsLib <> lift def
848
R10066:10068 Coq.Init.Datatypes <> snd def
849
R10038:10040 Coq.Init.Datatypes <> fst def
850
R10043:10044 Coq.Lists.Streams <> hd def
851
R10046:10047 StreamsLib <> s' var
852
prf 10093:10108 <> history_rec_spec
853
R10130:10135 Coq.Lists.Streams <> Stream coind
854
R10137:10137 StreamsLib <> A var
855
R10176:10182 Coq.Init.Logic <> :type_scope:x_'/\'_x not
856
R10172:10174 Coq.Init.Logic <> :type_scope:x_'='_x not
857
R10146:10148 Coq.Init.Datatypes <> fst def
858
R10151:10152 Coq.Lists.Streams <> hd def
859
R10155:10165 StreamsLib <> history_rec def
860
R10169:10169 StreamsLib <> s var
861
R10167:10167 StreamsLib <> p var
862
R10175:10175 StreamsLib <> p var
863
R10183:10188 Coq.Lists.Streams <> ForAll coind
864
R10232:10242 StreamsLib <> history_rec def
865
R10246:10246 StreamsLib <> s var
866
R10244:10244 StreamsLib <> p var
867
R10201:10212 StreamsLib <> History_Spec def
868
R10227:10228 StreamsLib <> s' var
869
R10215:10220 StreamsLib <> concat def
870
R10224:10224 StreamsLib <> s var
871
R10222:10222 StreamsLib <> p var
872
R10359:10372 Coq.Lists.Streams <> HereAndFurther constr
873
R10359:10372 Coq.Lists.Streams <> HereAndFurther constr
874
R10436:10446 StreamsLib <> eqst_concat thm
875
R10436:10446 StreamsLib <> eqst_concat thm
876
R10458:10474 StreamsLib <> unzip_history_rec thm
877
R10458:10474 StreamsLib <> unzip_history_rec thm
878
R10494:10497 Coq.Init.Datatypes <> cons constr
879
R10494:10497 Coq.Init.Datatypes <> cons constr
880
prf 10524:10535 <> history_spec
881
R10555:10560 Coq.Lists.Streams <> Stream coind
882
R10562:10562 StreamsLib <> A var
883
R10597:10602 Coq.Init.Logic <> :type_scope:x_'/\'_x not
884
R10591:10593 Coq.Init.Logic <> :type_scope:x_'='_x not
885
R10571:10573 Coq.Init.Datatypes <> fst def
886
R10576:10577 Coq.Lists.Streams <> hd def
887
R10580:10586 StreamsLib <> history def
888
R10588:10588 StreamsLib <> s var
889
R10594:10596 Coq.Init.Datatypes <> nil constr
890
R10603:10608 Coq.Lists.Streams <> ForAll coind
891
R10641:10647 StreamsLib <> history def
892
R10649:10649 StreamsLib <> s var
893
R10621:10632 StreamsLib <> History_Spec def
894
R10636:10637 StreamsLib <> s' var
895
R10634:10634 StreamsLib <> s var
896
R10680:10695 StreamsLib <> history_rec_spec thm
897
R10697:10699 Coq.Init.Datatypes <> nil constr
898
R10680:10695 StreamsLib <> history_rec_spec thm
899
R10697:10699 Coq.Init.Datatypes <> nil constr
900
R0:-1 StreamsLib <> y var
901
prf 10730:10754 <> history_rec_spec_complete
902
R10776:10781 Coq.Lists.Streams <> Stream coind
903
R10783:10783 StreamsLib <> A var
904
R10865:10868 Coq.Lists.Streams <> EqSt coind
905
R10874:10884 StreamsLib <> history_rec def
906
R10888:10888 StreamsLib <> s var
907
R10886:10886 StreamsLib <> p var
908
R10870:10871 StreamsLib <> ps var
909
R10811:10816 Coq.Lists.Streams <> ForAll coind
910
R10859:10860 StreamsLib <> ps var
911
R10829:10840 StreamsLib <> History_Spec def
912
R10855:10856 StreamsLib <> s' var
913
R10843:10848 StreamsLib <> concat def
914
R10852:10852 StreamsLib <> s var
915
R10850:10850 StreamsLib <> p var
916
R10803:10805 Coq.Init.Logic <> :type_scope:x_'='_x not
917
R10792:10794 Coq.Init.Datatypes <> fst def
918
R10797:10798 Coq.Lists.Streams <> hd def
919
R10800:10801 StreamsLib <> ps var
920
R10806:10806 StreamsLib <> p var
921
R11031:11042 StreamsLib <> History_Spec def
922
R11080:11083 Coq.Lists.Streams <> eqst constr
923
R11080:11083 Coq.Lists.Streams <> eqst constr
924
R11147:11158 StreamsLib <> History_Spec def
925
R11212:11222 StreamsLib <> concat_eqst thm
926
R11232:11241 Coq.Init.Logic <> refl_equal syndef
927
R11212:11222 StreamsLib <> concat_eqst thm
928
R11232:11241 Coq.Init.Logic <> refl_equal syndef
929
R11349:11359 StreamsLib <> concat_eqst thm
930
R11369:11378 Coq.Init.Logic <> refl_equal syndef
931
R11349:11359 StreamsLib <> concat_eqst thm
932
R11369:11378 Coq.Init.Logic <> refl_equal syndef
933
prf 11468:11488 <> history_spec_complete
934
R11508:11513 Coq.Lists.Streams <> Stream coind
935
R11515:11515 StreamsLib <> A var
936
R11588:11591 Coq.Lists.Streams <> EqSt coind
937
R11597:11603 StreamsLib <> history def
938
R11605:11605 StreamsLib <> s var
939
R11593:11594 StreamsLib <> ps var
940
R11545:11550 Coq.Lists.Streams <> ForAll coind
941
R11582:11583 StreamsLib <> ps var
942
R11563:11574 StreamsLib <> History_Spec def
943
R11578:11579 StreamsLib <> s' var
944
R11576:11576 StreamsLib <> s var
945
R11535:11537 Coq.Init.Logic <> :type_scope:x_'='_x not
946
R11524:11526 Coq.Init.Datatypes <> fst def
947
R11529:11530 Coq.Lists.Streams <> hd def
948
R11532:11533 StreamsLib <> ps var
949
R11538:11540 Coq.Init.Datatypes <> nil constr
950
R11630:11654 StreamsLib <> history_rec_spec_complete thm
951
R11630:11654 StreamsLib <> history_rec_spec_complete thm
952
prf 11698:11722 <> inv_snd_history_rec_intro
953
R11742:11747 Coq.Lists.Streams <> Stream coind
954
R11749:11749 StreamsLib <> A var
955
R11767:11772 Coq.Lists.Streams <> Stream coind
956
R11774:11774 StreamsLib <> A var
957
R11794:11799 Coq.Lists.Streams <> ForAll coind
958
R11845:11855 StreamsLib <> history_rec def
959
R11859:11859 StreamsLib <> s var
960
R11857:11857 StreamsLib <> p var
961
R11812:11812 StreamsLib <> P var
962
R11815:11819 StreamsLib <> apply def
963
R11839:11840 StreamsLib <> s' var
964
R11822:11825 StreamsLib <> lift def
965
R11829:11831 Coq.Init.Datatypes <> snd def
966
R11780:11785 Coq.Lists.Streams <> ForAll coind
967
R11789:11789 StreamsLib <> s var
968
R11787:11787 StreamsLib <> P var
969
R11884:11890 StreamsLib <> inv_map thm
970
R11884:11890 StreamsLib <> inv_map thm
971
R11905:11911 StreamsLib <> eqst_eq prfax
972
R11918:11934 StreamsLib <> unzip_history_rec thm
973
R11905:11911 StreamsLib <> eqst_eq prfax
974
R11918:11934 StreamsLib <> unzip_history_rec thm
975
prf 11995:12015 <> inv_snd_history_intro
976
R12035:12040 Coq.Lists.Streams <> Stream coind
977
R12042:12042 StreamsLib <> A var
978
R12058:12063 Coq.Lists.Streams <> Stream coind
979
R12065:12065 StreamsLib <> A var
980
R12085:12090 Coq.Lists.Streams <> ForAll coind
981
R12136:12142 StreamsLib <> history def
982
R12144:12144 StreamsLib <> s var
983
R12103:12103 StreamsLib <> P var
984
R12106:12110 StreamsLib <> apply def
985
R12130:12131 StreamsLib <> s' var
986
R12113:12116 StreamsLib <> lift def
987
R12120:12122 Coq.Init.Datatypes <> snd def
988
R12071:12076 Coq.Lists.Streams <> ForAll coind
989
R12080:12080 StreamsLib <> s var
990
R12078:12078 StreamsLib <> P var
991
R12169:12193 StreamsLib <> inv_snd_history_rec_intro thm
992
R12169:12193 StreamsLib <> inv_snd_history_rec_intro thm
993
prf 12222:12245 <> inv_snd_history_rec_elim
994
R12265:12270 Coq.Lists.Streams <> Stream coind
995
R12272:12272 StreamsLib <> A var
996
R12290:12295 Coq.Lists.Streams <> Stream coind
997
R12297:12297 StreamsLib <> A var
998
R12374:12379 Coq.Lists.Streams <> ForAll coind
999
R12383:12383 StreamsLib <> s var
1000
R12381:12381 StreamsLib <> P var
1001
R12303:12308 Coq.Lists.Streams <> ForAll coind
1002
R12354:12364 StreamsLib <> history_rec def
1003
R12368:12368 StreamsLib <> s var
1004
R12366:12366 StreamsLib <> p var
1005
R12321:12321 StreamsLib <> P var
1006
R12324:12328 StreamsLib <> apply def
1007
R12348:12349 StreamsLib <> s' var
1008
R12331:12334 StreamsLib <> lift def
1009
R12338:12340 Coq.Init.Datatypes <> snd def
1010
R12413:12419 StreamsLib <> eqst_eq prfax
1011
R12426:12442 StreamsLib <> unzip_history_rec thm
1012
R12413:12419 StreamsLib <> eqst_eq prfax
1013
R12426:12442 StreamsLib <> unzip_history_rec thm
1014
R12457:12463 StreamsLib <> map_inv thm
1015
R12457:12463 StreamsLib <> map_inv thm
1016
prf 12489:12508 <> inv_snd_history_elim
1017
R12528:12533 Coq.Lists.Streams <> Stream coind
1018
R12535:12535 StreamsLib <> A var
1019
R12551:12556 Coq.Lists.Streams <> Stream coind
1020
R12558:12558 StreamsLib <> A var
1021
R12629:12634 Coq.Lists.Streams <> ForAll coind
1022
R12638:12638 StreamsLib <> s var
1023
R12636:12636 StreamsLib <> P var
1024
R12564:12569 Coq.Lists.Streams <> ForAll coind
1025
R12615:12621 StreamsLib <> history def
1026
R12623:12623 StreamsLib <> s var
1027
R12582:12582 StreamsLib <> P var
1028
R12585:12589 StreamsLib <> apply def
1029
R12609:12610 StreamsLib <> s' var
1030
R12592:12595 StreamsLib <> lift def
1031
R12599:12601 Coq.Init.Datatypes <> snd def
1032
R12698:12700 Coq.Init.Datatypes <> nil constr
1033
R12662:12685 StreamsLib <> inv_snd_history_rec_elim thm
1034
R12698:12700 Coq.Init.Datatypes <> nil constr
1035
R12662:12685 StreamsLib <> inv_snd_history_rec_elim thm
1036
def 12731:12736 <> prefix
1037
R12747:12747 StreamsLib <> A var
1038
R12768:12768 StreamsLib <> A var
1039
R12763:12763 StreamsLib <> A var
1040
R12784:12786 Coq.Init.Datatypes <> nat ind
1041
R12791:12794 Coq.Init.Datatypes <> list ind
1042
R12796:12796 StreamsLib <> A var
1043
R12817:12817 StreamsLib <> k var
1044
R12849:12852 Coq.Init.Logic <> True ind
1045
R12858:12858 Coq.Init.Datatypes <> S constr
1046
R12884:12884 StreamsLib <> p var
1047
R12916:12919 Coq.Init.Logic <> True ind
1048
R12986:12986 StreamsLib <> I var
1049
R13016:13016 Coq.Init.Logic <> :type_scope:x_'/\'_x not
1050
R13023:13028 Coq.Init.Logic <> :type_scope:x_'/\'_x not
1051
R13044:13044 Coq.Init.Logic <> :type_scope:x_'/\'_x not
1052
R13017:13017 StreamsLib <> T var
1053
R13029:13034 StreamsLib <> prefix def
1054
R13038:13038 StreamsLib <> T var
1055
R13036:13036 StreamsLib <> I var
1056
prf 13077:13089 <> prefix_mono_k
1057
R13115:13118 Coq.Init.Datatypes <> list ind
1058
R13120:13120 StreamsLib <> A var
1059
R13146:13151 StreamsLib <> prefix def
1060
R13159:13159 StreamsLib <> p var
1061
R13157:13157 StreamsLib <> k var
1062
R13155:13155 StreamsLib <> T var
1063
R13153:13153 StreamsLib <> I var
1064
R13124:13129 StreamsLib <> prefix def
1065
R13141:13141 StreamsLib <> p var
1066
R13136:13136 Coq.Init.Datatypes <> S constr
1067
R13138:13138 StreamsLib <> k var
1068
R13133:13133 StreamsLib <> T var
1069
R13131:13131 StreamsLib <> I var
1070
R0:-1 StreamsLib <> y var
1071
R0:-1 StreamsLib <> y var
1072
R0:-1 StreamsLib <> y var
1073
R0:-1 StreamsLib <> y var
1074
R0:-1 StreamsLib <> y var
1075
prf 13316:13327 <> prefix_apply
1076
R13350:13350 StreamsLib <> A var
1077
R13374:13374 StreamsLib <> A var
1078
R13369:13369 StreamsLib <> A var
1079
R13392:13395 Coq.Init.Datatypes <> list ind
1080
R13397:13397 StreamsLib <> A var
1081
R13490:13495 StreamsLib <> prefix def
1082
R13505:13505 StreamsLib <> p var
1083
R13503:13503 StreamsLib <> k var
1084
R13500:13501 StreamsLib <> T' var
1085
R13497:13498 StreamsLib <> I' var
1086
R13421:13426 StreamsLib <> prefix def
1087
R13485:13485 StreamsLib <> p var
1088
R13483:13483 StreamsLib <> k var
1089
R13474:13475 StreamsLib <> T' var
1090
R13479:13480 StreamsLib <> s' var
1091
R13477:13477 StreamsLib <> s var
1092
R13464:13464 StreamsLib <> T var
1093
R13468:13469 StreamsLib <> s' var
1094
R13466:13466 StreamsLib <> s var
1095
R13445:13446 StreamsLib <> I' var
1096
R13448:13448 StreamsLib <> s var
1097
R13438:13438 StreamsLib <> I var
1098
R13440:13440 StreamsLib <> s var
1099
R13403:13408 StreamsLib <> prefix def
1100
R13416:13416 StreamsLib <> p var
1101
R13414:13414 StreamsLib <> k var
1102
R13412:13412 StreamsLib <> T var
1103
R13410:13410 StreamsLib <> I var
1104
R0:-1 StreamsLib <> y var
1105
R0:-1 StreamsLib <> y var
1106
prf 13649:13658 <> kinduction
1107
R13678:13678 StreamsLib <> A var
1108
R13696:13701 Coq.Lists.Streams <> Stream coind
1109
R13703:13703 StreamsLib <> A var
1110
R13827:13832 Coq.Lists.Streams <> ForAll coind
1111
R13856:13856 StreamsLib <> s var
1112
R13845:13845 StreamsLib <> P var
1113
R13848:13849 Coq.Lists.Streams <> hd def
1114
R13851:13852 StreamsLib <> s' var
1115
R13711:13716 Coq.Lists.Streams <> ForAll coind
1116
R13812:13818 StreamsLib <> history def
1117
R13820:13820 StreamsLib <> s var
1118
R13794:13794 StreamsLib <> P var
1119
R13797:13799 Coq.Init.Datatypes <> snd def
1120
R13802:13803 Coq.Lists.Streams <> hd def
1121
R13805:13806 StreamsLib <> s' var
1122
R13729:13734 StreamsLib <> prefix def
1123
R13778:13780 Coq.Init.Datatypes <> fst def
1124
R13783:13784 Coq.Lists.Streams <> hd def
1125
R13786:13787 StreamsLib <> s' var
1126
R13775:13775 StreamsLib <> k var
1127
R13768:13768 StreamsLib <> P var
1128
R13770:13772 StreamsLib <> st' var
1129
R13747:13747 StreamsLib <> P var
1130
R13749:13750 StreamsLib <> st var
1131
R13880:13899 StreamsLib <> inv_snd_history_elim thm
1132
R13880:13899 StreamsLib <> inv_snd_history_elim thm
1133
R13946:13948 Coq.Init.Datatypes <> snd def
1134
R13951:13952 Coq.Lists.Streams <> hd def
1135
R13954:13955 StreamsLib <> s' var
1136
R13909:13920 StreamsLib <> ForAll_apply def
1137
R13946:13948 Coq.Init.Datatypes <> snd def
1138
R13951:13952 Coq.Lists.Streams <> hd def
1139
R13954:13955 StreamsLib <> s' var
1140
R13909:13920 StreamsLib <> ForAll_apply def
1141
R14024:14029 StreamsLib <> prefix def
1142
R14073:14075 Coq.Init.Datatypes <> fst def
1143
R14078:14079 Coq.Lists.Streams <> hd def
1144
R14081:14082 StreamsLib <> s' var
1145
R14065:14067 StreamsLib <> st' var
1146
R14044:14045 StreamsLib <> st var
1147
R13971:13982 StreamsLib <> ForAll_apply def
1148
R14024:14029 StreamsLib <> prefix def
1149
R14073:14075 Coq.Init.Datatypes <> fst def
1150
R14078:14079 Coq.Lists.Streams <> hd def
1151
R14081:14082 StreamsLib <> s' var
1152
R14065:14067 StreamsLib <> st' var
1153
R14044:14045 StreamsLib <> st var
1154
R13971:13982 StreamsLib <> ForAll_apply def
1155
R14138:14143 Coq.Lists.Streams <> ForAll coind
1156
R14169:14174 Coq.Lists.Streams <> Stream coind
1157
R14183:14185 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
1158
R14177:14180 Coq.Init.Datatypes <> list ind
1159
R14299:14301 Coq.Init.Datatypes <> snd def
1160
R14304:14305 Coq.Lists.Streams <> hd def
1161
R14307:14308 StreamsLib <> s' var
1162
R14207:14212 StreamsLib <> prefix def
1163
R14280:14282 Coq.Init.Datatypes <> fst def
1164
R14285:14286 Coq.Lists.Streams <> hd def
1165
R14288:14289 StreamsLib <> s' var
1166
R14255:14257 StreamsLib <> st' var
1167
R14231:14232 StreamsLib <> st var
1168
R14100:14115 StreamsLib <> ForAll_reinforce def
1169
R14138:14143 Coq.Lists.Streams <> ForAll coind
1170
R14169:14174 Coq.Lists.Streams <> Stream coind
1171
R14183:14185 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
1172
R14177:14180 Coq.Init.Datatypes <> list ind
1173
R14299:14301 Coq.Init.Datatypes <> snd def
1174
R14304:14305 Coq.Lists.Streams <> hd def
1175
R14307:14308 StreamsLib <> s' var
1176
R14207:14212 StreamsLib <> prefix def
1177
R14280:14282 Coq.Init.Datatypes <> fst def
1178
R14285:14286 Coq.Lists.Streams <> hd def
1179
R14288:14289 StreamsLib <> s' var
1180
R14255:14257 StreamsLib <> st' var
1181
R14231:14232 StreamsLib <> st var
1182
R14100:14115 StreamsLib <> ForAll_reinforce def
1183
R14359:14364 Coq.Lists.Streams <> ForAll coind
1184
R14376:14381 Coq.Lists.Streams <> Stream coind
1185
R14390:14392 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
1186
R14384:14387 Coq.Init.Datatypes <> list ind
1187
R14399:14410 StreamsLib <> History_Spec def
1188
R14414:14415 StreamsLib <> s' var
1189
R14327:14342 StreamsLib <> ForAll_reinforce def
1190
R14359:14364 Coq.Lists.Streams <> ForAll coind
1191
R14376:14381 Coq.Lists.Streams <> Stream coind
1192
R14390:14392 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
1193
R14384:14387 Coq.Init.Datatypes <> list ind
1194
R14399:14410 StreamsLib <> History_Spec def
1195
R14414:14415 StreamsLib <> s' var
1196
R14327:14342 StreamsLib <> ForAll_reinforce def
1197
R14429:14440 Coq.Lists.Streams <> ForAll_coind thm
1198
R14429:14440 Coq.Lists.Streams <> ForAll_coind thm
1199
R14472:14472 StreamsLib <> x var
1200
R14472:14472 StreamsLib <> x var
1201
R0:-1 StreamsLib <> y var
1202
R14646:14657 StreamsLib <> History_Spec def
1203
R0:-1 StreamsLib <> y var
1204
R14925:14937 StreamsLib <> prefix_mono_k thm
1205
R14925:14937 StreamsLib <> prefix_mono_k thm
1206
R0:-1 StreamsLib <> y var
1207
R14998:15009 StreamsLib <> history_spec thm
1208
R14998:15009 StreamsLib <> history_spec thm
1209
R0:-1 StreamsLib <> y var
1210
R15147:15159 StreamsLib <> necessitation def
1211
R15147:15159 StreamsLib <> necessitation def
1212
prf 15208:15218 <> kinduction'
1213
R15239:15239 StreamsLib <> A var
1214
R15260:15265 Coq.Lists.Streams <> Stream coind
1215
R15267:15267 StreamsLib <> A var
1216
R15448:15453 Coq.Lists.Streams <> ForAll coind
1217
R15477:15477 StreamsLib <> s var
1218
R15466:15466 StreamsLib <> P var
1219
R15469:15470 Coq.Lists.Streams <> hd def
1220
R15472:15473 StreamsLib <> s' var
1221
R15341:15346 Coq.Lists.Streams <> ForAll coind
1222
R15441:15442 StreamsLib <> ps var
1223
R15424:15424 StreamsLib <> P var
1224
R15427:15429 Coq.Init.Datatypes <> snd def
1225
R15432:15433 Coq.Lists.Streams <> hd def
1226
R15435:15436 StreamsLib <> s' var
1227
R15359:15364 StreamsLib <> prefix def
1228
R15408:15410 Coq.Init.Datatypes <> fst def
1229
R15413:15414 Coq.Lists.Streams <> hd def
1230
R15416:15417 StreamsLib <> s' var
1231
R15405:15405 StreamsLib <> k var
1232
R15398:15398 StreamsLib <> P var
1233
R15400:15402 StreamsLib <> st' var
1234
R15377:15377 StreamsLib <> P var
1235
R15379:15380 StreamsLib <> st var
1236
R15297:15302 Coq.Lists.Streams <> ForAll coind
1237
R15334:15335 StreamsLib <> ps var
1238
R15315:15326 StreamsLib <> History_Spec def
1239
R15330:15331 StreamsLib <> s' var
1240
R15328:15328 StreamsLib <> s var
1241
R15286:15288 Coq.Init.Logic <> :type_scope:x_'='_x not
1242
R15275:15277 Coq.Init.Datatypes <> fst def
1243
R15280:15281 Coq.Lists.Streams <> hd def
1244
R15283:15284 StreamsLib <> ps var
1245
R15289:15291 Coq.Init.Datatypes <> nil constr
1246
R15504:15510 StreamsLib <> eqst_eq prfax
1247
R15517:15537 StreamsLib <> history_spec_complete thm
1248
R15504:15510 StreamsLib <> eqst_eq prfax
1249
R15517:15537 StreamsLib <> history_spec_complete thm
1250
R15564:15573 StreamsLib <> kinduction thm
1251
R15564:15573 StreamsLib <> kinduction thm
1252
prf 15600:15621 <> inv_prefix_history_rec
1253
R15641:15641 StreamsLib <> A var
1254
R15662:15662 StreamsLib <> A var
1255
R15657:15657 StreamsLib <> A var
1256
R15680:15685 Coq.Lists.Streams <> Stream coind
1257
R15687:15687 StreamsLib <> A var
1258
R15799:15804 Coq.Lists.Streams <> ForAll coind
1259
R15867:15877 StreamsLib <> history_rec def
1260
R15881:15881 StreamsLib <> s var
1261
R15879:15879 StreamsLib <> p var
1262
R15817:15822 StreamsLib <> prefix def
1263
R15831:15834 Coq.Init.Datatypes <> cons constr
1264
R15851:15853 Coq.Init.Datatypes <> fst def
1265
R15856:15857 Coq.Lists.Streams <> hd def
1266
R15859:15860 StreamsLib <> s' var
1267
R15837:15839 Coq.Init.Datatypes <> snd def
1268
R15842:15843 Coq.Lists.Streams <> hd def
1269
R15845:15846 StreamsLib <> s' var
1270
R15828:15828 StreamsLib <> k var
1271
R15826:15826 StreamsLib <> T var
1272
R15824:15824 StreamsLib <> I var
1273
R15764:15769 StreamsLib <> prefix def
1274
R15778:15781 Coq.Init.Datatypes <> cons constr
1275
R15790:15790 StreamsLib <> p var
1276
R15784:15785 Coq.Lists.Streams <> hd def
1277
R15787:15787 StreamsLib <> s var
1278
R15775:15775 StreamsLib <> k var
1279
R15773:15773 StreamsLib <> T var
1280
R15771:15771 StreamsLib <> I var
1281
R15692:15697 Coq.Lists.Streams <> ForAll coind
1282
R15735:15740 StreamsLib <> concat def
1283
R15744:15744 StreamsLib <> s var
1284
R15742:15742 StreamsLib <> p var
1285
R15710:15710 StreamsLib <> T var
1286
R15721:15722 Coq.Lists.Streams <> hd def
1287
R15725:15726 Coq.Lists.Streams <> tl def
1288
R15728:15729 StreamsLib <> s' var
1289
R15713:15714 Coq.Lists.Streams <> hd def
1290
R15716:15717 StreamsLib <> s' var
1291
R15970:15983 Coq.Lists.Streams <> HereAndFurther constr
1292
R15970:15983 Coq.Lists.Streams <> HereAndFurther constr
1293
R16097:16106 StreamsLib <> inv_concat thm
1294
R16097:16106 StreamsLib <> inv_concat thm
1295
R16184:16196 StreamsLib <> prefix_mono_k thm
1296
R16184:16196 StreamsLib <> prefix_mono_k thm
1297
prf 16229:16246 <> inv_prefix_history
1298
R16266:16266 StreamsLib <> A var
1299
R16287:16287 StreamsLib <> A var
1300
R16282:16282 StreamsLib <> A var
1301
R16303:16308 Coq.Lists.Streams <> Stream coind
1302
R16310:16310 StreamsLib <> A var
1303
R16386:16391 Coq.Lists.Streams <> ForAll coind
1304
R16454:16460 StreamsLib <> history def
1305
R16462:16462 StreamsLib <> s var
1306
R16404:16409 StreamsLib <> prefix def
1307
R16418:16421 Coq.Init.Datatypes <> cons constr
1308
R16438:16440 Coq.Init.Datatypes <> fst def
1309
R16443:16444 Coq.Lists.Streams <> hd def
1310
R16446:16447 StreamsLib <> s' var
1311
R16424:16426 Coq.Init.Datatypes <> snd def
1312
R16429:16430 Coq.Lists.Streams <> hd def
1313
R16432:16433 StreamsLib <> s' var
1314
R16415:16415 StreamsLib <> k var
1315
R16413:16413 StreamsLib <> T var
1316
R16411:16411 StreamsLib <> I var
1317
R16327:16332 Coq.Lists.Streams <> ForAll coind
1318
R16369:16369 StreamsLib <> s var
1319
R16345:16345 StreamsLib <> T var
1320
R16356:16357 Coq.Lists.Streams <> hd def
1321
R16360:16361 Coq.Lists.Streams <> tl def
1322
R16363:16364 StreamsLib <> s' var
1323
R16348:16349 Coq.Lists.Streams <> hd def
1324
R16351:16352 StreamsLib <> s' var
1325
R16315:16315 StreamsLib <> I var
1326
R16318:16319 Coq.Lists.Streams <> hd def
1327
R16321:16321 StreamsLib <> s var
1328
R16487:16508 StreamsLib <> inv_prefix_history_rec thm
1329
R16487:16508 StreamsLib <> inv_prefix_history_rec thm
1330
prf 16585:16603 <> inv_prefix_history'
1331
R16623:16623 StreamsLib <> A var
1332
R16644:16644 StreamsLib <> A var
1333
R16639:16639 StreamsLib <> A var
1334
R16660:16665 Coq.Lists.Streams <> Stream coind
1335
R16667:16667 StreamsLib <> A var
1336
R16743:16748 Coq.Lists.Streams <> ForAll coind
1337
R16790:16796 StreamsLib <> history def
1338
R16798:16798 StreamsLib <> s var
1339
R16761:16766 StreamsLib <> prefix def
1340
R16775:16777 Coq.Init.Datatypes <> fst def
1341
R16780:16781 Coq.Lists.Streams <> hd def
1342
R16783:16784 StreamsLib <> s' var
1343
R16772:16772 StreamsLib <> k var
1344
R16770:16770 StreamsLib <> T var
1345
R16768:16768 StreamsLib <> I var
1346
R16684:16689 Coq.Lists.Streams <> ForAll coind
1347
R16726:16726 StreamsLib <> s var
1348
R16702:16702 StreamsLib <> T var
1349
R16713:16714 Coq.Lists.Streams <> hd def
1350
R16717:16718 Coq.Lists.Streams <> tl def
1351
R16720:16721 StreamsLib <> s' var
1352
R16705:16706 Coq.Lists.Streams <> hd def
1353
R16708:16709 StreamsLib <> s' var
1354
R16672:16672 StreamsLib <> I var
1355
R16675:16676 Coq.Lists.Streams <> hd def
1356
R16678:16678 StreamsLib <> s var
1357
R16836:16848 StreamsLib <> necessitation def
1358
R16836:16848 StreamsLib <> necessitation def
1359
R16878:16889 StreamsLib <> ForAll_apply def
1360
R16878:16889 StreamsLib <> ForAll_apply def
1361
R16912:16929 StreamsLib <> inv_prefix_history thm
1362
R16942:16942 Coq.Init.Datatypes <> S constr
1363
R16945:16945 Coq.Init.Datatypes <> S constr
1364
R16939:16939 StreamsLib <> n var
1365
R16937:16937 StreamsLib <> i var
1366
R16912:16929 StreamsLib <> inv_prefix_history thm
1367
R16942:16942 Coq.Init.Datatypes <> S constr
1368
R16945:16945 Coq.Init.Datatypes <> S constr
1369
R16939:16939 StreamsLib <> n var
1370
R16937:16937 StreamsLib <> i var
1371
R16988:17000 StreamsLib <> necessitation def
1372
R16988:17000 StreamsLib <> necessitation def
1373
R0:-1 StreamsLib <> y var
1374
def 17105:17113 <> effective
1375
R17131:17138 Coq.Relations.Relation_Definitions <> relation def
1376
R17140:17140 StreamsLib <> A var
1377
R17161:17162 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
1378
R17170:17176 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
1379
R17186:17187 Coq.Init.Specif <> :type_scope:'{'_x_'}'_'+'_'{'_x_'}' not
1380
R17163:17163 StreamsLib <> r var
1381
R17168:17169 StreamsLib <> a2 var
1382
R17165:17166 StreamsLib <> a1 var
1383
R17177:17178 Coq.Init.Logic <> :type_scope:'~'_x not
1384
R17179:17179 StreamsLib <> r var
1385
R17184:17185 StreamsLib <> a2 var
1386
R17181:17182 StreamsLib <> a1 var
1387
def 17202:17208 <> lift_hd
1388
R17226:17233 Coq.Relations.Relation_Definitions <> relation def
1389
R17235:17235 StreamsLib <> A var
1390
R17240:17247 Coq.Relations.Relation_Definitions <> relation def
1391
R17250:17255 Coq.Lists.Streams <> Stream coind
1392
R17257:17257 StreamsLib <> A var
1393
R17284:17284 StreamsLib <> r var
1394
R17295:17296 Coq.Lists.Streams <> hd def
1395
R17298:17299 StreamsLib <> s2 var
1396
R17287:17288 Coq.Lists.Streams <> hd def
1397
R17290:17291 StreamsLib <> s1 var
1398
prf 17312:17328 <> lift_hd_effective
1399
R17355:17362 Coq.Relations.Relation_Definitions <> relation def
1400
R17364:17364 StreamsLib <> A var
1401
R17384:17392 StreamsLib <> effective def
1402
R17395:17401 StreamsLib <> lift_hd def
1403
R17403:17403 StreamsLib <> r var
1404
R17369:17377 StreamsLib <> effective def
1405
R17379:17379 StreamsLib <> r var
1406
R17421:17429 StreamsLib <> effective def
1407
R17432:17438 StreamsLib <> lift_hd def
1408
sec 17522:17531 <> FixedPoint
1409
var 17544:17544 FixedPoint A
1410
var 17563:17567 FixedPoint union
1411
R17581:17581 StreamsLib <> FixedPoint.A var
1412
R17576:17576 StreamsLib <> FixedPoint.A var
1413
R17571:17571 StreamsLib <> FixedPoint.A var
1414
var 17594:17595 FixedPoint le
1415
R17599:17606 Coq.Relations.Relation_Definitions <> relation def
1416
R17608:17608 StreamsLib <> FixedPoint.A var
1417
var 17623:17629 FixedPoint le_mono
1418
R17645:17646 StreamsLib <> FixedPoint.le var
1419
R17651:17655 StreamsLib <> FixedPoint.union var
1420
R17659:17659 StreamsLib <> y var
1421
R17657:17657 StreamsLib <> x var
1422
R17648:17648 StreamsLib <> x var
1423
var 17675:17680 FixedPoint le_eff
1424
R17684:17692 StreamsLib <> effective def
1425
R17694:17695 StreamsLib <> FixedPoint.le var
1426
def 17710:17711 <> gt
1427
R17726:17729 Coq.Init.Logic <> :type_scope:x_'/\'_x not
1428
R17720:17721 StreamsLib <> FixedPoint.le var
1429
R17725:17725 StreamsLib <> x var
1430
R17723:17723 StreamsLib <> y var
1431
R17730:17731 Coq.Init.Logic <> :type_scope:'~'_x not
1432
R17732:17733 StreamsLib <> FixedPoint.le var
1433
R17737:17737 StreamsLib <> y var
1434
R17735:17735 StreamsLib <> x var
1435
var 17752:17756 FixedPoint gt_wf
1436
R17760:17771 Coq.Init.Wf <> well_founded def
1437
R17773:17774 StreamsLib <> gt def
1438
fix 17795:17800 <> rec_hd
1439
R17819:17824 Coq.Lists.Streams <> Stream coind
1440
R17826:17826 StreamsLib <> FixedPoint.A var
1441
R17807:17812 Coq.Lists.Streams <> Stream coind
1442
R17814:17814 StreamsLib <> FixedPoint.A var
1443
R17834:17839 Coq.Lists.Streams <> Stream coind
1444
R17841:17841 StreamsLib <> FixedPoint.A var
1445
R17868:17873 Coq.Lists.Streams <> Stream coind
1446
R17875:17875 StreamsLib <> FixedPoint.A var
1447
R17850:17856 StreamsLib <> lift_hd def
1448
R17858:17859 StreamsLib <> gt def
1449
R17891:17895 StreamsLib <> apply def
1450
R17898:17902 StreamsLib <> apply def
1451
R17905:17908 StreamsLib <> lift def
1452
R17910:17914 StreamsLib <> FixedPoint.union var
1453
R17934:17950 StreamsLib <> lift_hd_effective thm
1454
R17959:17960 StreamsLib <> s' var
1455
R17952:17957 StreamsLib <> FixedPoint.le_eff var
1456
R17980:17985 StreamsLib <> rec_hd def
1457
R17989:17990 StreamsLib <> s' var
1458
R17971:17972 StreamsLib <> s' var
1459
R18022:18028 StreamsLib <> lift_hd def
1460
R18039:18046 StreamsLib <> hd_apply thm
1461
R18039:18046 StreamsLib <> hd_apply thm
1462
R18057:18064 StreamsLib <> hd_apply thm
1463
R18057:18064 StreamsLib <> hd_apply thm
1464
R18075:18081 StreamsLib <> hd_lift thm
1465
R18075:18081 StreamsLib <> hd_lift thm
1466
R18091:18092 StreamsLib <> gt def
1467
R18109:18115 StreamsLib <> FixedPoint.le_mono var
1468
R18109:18115 StreamsLib <> FixedPoint.le_mono var
1469
R18127:18133 StreamsLib <> lift_hd def
1470
R18150:18157 StreamsLib <> hd_apply thm
1471
R18150:18157 StreamsLib <> hd_apply thm
1472
R18174:18181 StreamsLib <> hd_apply thm
1473
R18174:18181 StreamsLib <> hd_apply thm
1474
R18198:18204 StreamsLib <> hd_lift thm
1475
R18198:18204 StreamsLib <> hd_lift thm
1476
R18256:18257 Coq.Program.Wf <> MR def
1477
R18266:18281 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
1478
R18266:18281 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
1479
R18291:18297 StreamsLib <> lift_hd def
1480
R18306:18321 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
1481
R18306:18321 Coq.Wellfounded.Inverse_Image <> wf_inverse_image thm
1482
def 18357:18359 <> rec
1483
R18378:18383 Coq.Lists.Streams <> Stream coind
1484
R18385:18385 StreamsLib <> FixedPoint.A var
1485
R18366:18371 Coq.Lists.Streams <> Stream coind
1486
R18373:18373 StreamsLib <> FixedPoint.A var
1487
R18393:18398 Coq.Lists.Streams <> Stream coind
1488
R18400:18400 StreamsLib <> FixedPoint.A var
1489
R18405:18410 Coq.Lists.Streams <> Stream coind
1490
R18412:18412 StreamsLib <> FixedPoint.A var
1491
R18428:18433 StreamsLib <> rec_hd def
1492
R18437:18437 StreamsLib <> s var
1493
R18435:18435 StreamsLib <> f var
1494
R18442:18445 Coq.Lists.Streams <> Cons constr
1495
R18456:18458 StreamsLib <> rec def
1496
R18463:18464 Coq.Lists.Streams <> tl def
1497
R18466:18467 StreamsLib <> s' var
1498
R18460:18460 StreamsLib <> f var
1499
R18448:18449 Coq.Lists.Streams <> hd def
1500
R18451:18452 StreamsLib <> s' var
1501
R18477:18486 StreamsLib FixedPoint <> sec