-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLists.glob
1235 lines (1235 loc) · 51.3 KB
/
Lists.glob
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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
DIGEST f9067acb73e2066cfb0b3f00ef2937a4
FLists
R93:101 Induction <> <> lib
mod 111:117 <> NatList
R126:128 Basics <> day ind
ind 422:428 NatList natprod
constr 442:445 NatList pair
R452:455 Coq.Init.Logic <> :type_scope:x_'->'_x not
R459:462 Coq.Init.Logic <> :type_scope:x_'->'_x not
R463:469 Lists <> natprod ind
R456:458 Coq.Init.Datatypes <> nat ind
R449:451 Coq.Init.Datatypes <> nat ind
R649:652 Lists NatList pair constr
def 866:868 NatList fst
R875:881 Lists NatList natprod ind
R886:888 Coq.Init.Datatypes <> nat ind
R901:901 Lists <> p var
R912:915 Lists NatList pair constr
def 945:947 NatList snd
R954:960 Lists NatList natprod ind
R965:967 Coq.Init.Datatypes <> nat ind
R980:980 Lists <> p var
R991:994 Lists NatList pair constr
R1022:1024 Lists NatList fst def
R1027:1030 Lists NatList pair constr
R1301:1304 Lists NatList pair constr
not 1285:1285 NatList ::'('_x_','_x_')'
R1623:1625 Lists NatList fst def
R1627:1627 Lists NatList ::'('_x_','_x_')' not
R1629:1629 Lists NatList ::'('_x_','_x_')' not
R1631:1631 Lists NatList ::'('_x_','_x_')' not
def 1647:1650 NatList fst'
R1657:1663 Lists NatList natprod ind
R1668:1670 Coq.Init.Datatypes <> nat ind
R1683:1683 Lists <> p var
R1694:1694 Lists NatList ::'('_x_','_x_')' not
R1696:1696 Lists NatList ::'('_x_','_x_')' not
R1698:1698 Lists NatList ::'('_x_','_x_')' not
def 1724:1727 NatList snd'
R1734:1740 Lists NatList natprod ind
R1745:1747 Coq.Init.Datatypes <> nat ind
R1760:1760 Lists <> p var
R1771:1771 Lists NatList ::'('_x_','_x_')' not
R1773:1773 Lists NatList ::'('_x_','_x_')' not
R1775:1775 Lists NatList ::'('_x_','_x_')' not
def 1801:1809 NatList swap_pair
R1816:1822 Lists NatList natprod ind
R1827:1833 Lists NatList natprod ind
R1846:1846 Lists <> p var
R1857:1857 Lists NatList ::'('_x_','_x_')' not
R1859:1859 Lists NatList ::'('_x_','_x_')' not
R1861:1861 Lists NatList ::'('_x_','_x_')' not
R1866:1866 Lists NatList ::'('_x_','_x_')' not
R1868:1868 Lists NatList ::'('_x_','_x_')' not
R1870:1870 Lists NatList ::'('_x_','_x_')' not
prf 2104:2122 NatList surjective_pairing'
R2140:2142 Coq.Init.Datatypes <> nat ind
R2153:2155 Coq.Init.Logic <> :type_scope:x_'='_x not
R2148:2148 Lists NatList ::'('_x_','_x_')' not
R2150:2150 Lists NatList ::'('_x_','_x_')' not
R2152:2152 Lists NatList ::'('_x_','_x_')' not
R2149:2149 Lists <> n var
R2151:2151 Lists <> m var
R2156:2156 Lists NatList ::'('_x_','_x_')' not
R2166:2167 Lists NatList ::'('_x_','_x_')' not
R2177:2177 Lists NatList ::'('_x_','_x_')' not
R2157:2159 Lists NatList fst def
R2161:2161 Lists NatList ::'('_x_','_x_')' not
R2163:2163 Lists NatList ::'('_x_','_x_')' not
R2165:2165 Lists NatList ::'('_x_','_x_')' not
R2162:2162 Lists <> n var
R2164:2164 Lists <> m var
R2168:2170 Lists NatList snd def
R2172:2172 Lists NatList ::'('_x_','_x_')' not
R2174:2174 Lists NatList ::'('_x_','_x_')' not
R2176:2176 Lists NatList ::'('_x_','_x_')' not
R2173:2173 Lists <> n var
R2175:2175 Lists <> m var
prf 2306:2329 NatList surjective_pairing_stuck
R2345:2351 Lists NatList natprod ind
R2358:2360 Coq.Init.Logic <> :type_scope:x_'='_x not
R2357:2357 Lists <> p var
R2361:2361 Lists NatList ::'('_x_','_x_')' not
R2367:2368 Lists NatList ::'('_x_','_x_')' not
R2374:2374 Lists NatList ::'('_x_','_x_')' not
R2362:2364 Lists NatList fst def
R2366:2366 Lists <> p var
R2369:2371 Lists NatList snd def
R2373:2373 Lists <> p var
prf 2594:2611 NatList surjective_pairing
R2627:2633 Lists NatList natprod ind
R2640:2642 Coq.Init.Logic <> :type_scope:x_'='_x not
R2639:2639 Lists <> p var
R2643:2643 Lists NatList ::'('_x_','_x_')' not
R2649:2650 Lists NatList ::'('_x_','_x_')' not
R2656:2656 Lists NatList ::'('_x_','_x_')' not
R2644:2646 Lists NatList fst def
R2648:2648 Lists <> p var
R2651:2653 Lists NatList snd def
R2655:2655 Lists <> p var
prf 2954:2968 NatList snd_fst_is_swap
R2984:2990 Lists NatList natprod ind
R3010:3012 Coq.Init.Logic <> :type_scope:x_'='_x not
R2996:2996 Lists NatList ::'('_x_','_x_')' not
R3002:3003 Lists NatList ::'('_x_','_x_')' not
R3009:3009 Lists NatList ::'('_x_','_x_')' not
R2997:2999 Lists NatList snd def
R3001:3001 Lists <> p var
R3004:3006 Lists NatList fst def
R3008:3008 Lists <> p var
R3013:3021 Lists NatList swap_pair def
R3023:3023 Lists <> p var
prf 3168:3182 NatList fst_swap_is_snd
R3198:3204 Lists NatList natprod ind
R3227:3229 Coq.Init.Logic <> :type_scope:x_'='_x not
R3210:3212 Lists NatList fst def
R3215:3223 Lists NatList swap_pair def
R3225:3225 Lists <> p var
R3230:3232 Lists NatList snd def
R3234:3234 Lists <> p var
ind 3610:3616 NatList natlist
constr 3632:3634 NatList nil
constr 3651:3654 NatList cons
R3639:3645 Lists <> natlist ind
R3661:3664 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3672:3675 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3676:3682 Lists <> natlist ind
R3665:3671 Lists <> natlist ind
R3658:3660 Coq.Init.Datatypes <> nat ind
def 3748:3753 NatList mylist
R3758:3761 Lists NatList cons constr
R3766:3769 Lists NatList cons constr
R3774:3777 Lists NatList cons constr
R3781:3783 Lists NatList nil constr
R4062:4065 Lists NatList cons constr
not 4049:4049 NatList ::x_'::'_x
R4147:4149 Lists NatList nil constr
not 4138:4138 NatList ::'['_']'
R4182:4185 Lists NatList cons constr
R4193:4196 Lists NatList cons constr
R4200:4202 Lists NatList nil constr
not 4161:4161 NatList ::'['_x_';'_'..'_';'_x_']'
def 4574:4580 NatList mylist1
R4586:4590 Lists NatList ::x_'::'_x not
R4606:4606 Lists NatList ::x_'::'_x not
R4592:4596 Lists NatList ::x_'::'_x not
R4605:4605 Lists NatList ::x_'::'_x not
R4598:4601 Lists NatList ::x_'::'_x not
R4602:4604 Lists NatList nil constr
def 4620:4626 NatList mylist2
R4632:4635 Lists NatList ::x_'::'_x not
R4637:4640 Lists NatList ::x_'::'_x not
R4642:4645 Lists NatList ::x_'::'_x not
R4646:4648 Lists NatList nil constr
def 4662:4668 NatList mylist3
R4673:4673 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R4675:4675 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R4677:4677 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R4679:4679 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 6113:6118 NatList repeat
R6131:6133 Coq.Init.Datatypes <> nat ind
R6138:6144 Lists NatList natlist ind
R6157:6161 Lists <> count var
R6172:6172 Coq.Init.Datatypes <> O constr
R6177:6179 Lists NatList nil constr
R6185:6185 Coq.Init.Datatypes <> S constr
R6198:6202 Lists NatList ::x_'::'_x not
R6218:6218 Lists NatList ::x_'::'_x not
R6197:6197 Lists <> n var
R6203:6208 Lists <> repeat def
R6210:6210 Lists <> n var
def 6391:6396 NatList length
R6401:6407 Lists NatList natlist ind
R6412:6414 Coq.Init.Datatypes <> nat ind
R6427:6427 Lists <> l var
R6438:6440 Lists NatList nil constr
R6445:6445 Coq.Init.Datatypes <> O constr
R6452:6455 Lists NatList ::x_'::'_x not
R6461:6461 Coq.Init.Datatypes <> S constr
R6464:6469 Lists <> length def
def 6643:6645 NatList app
R6656:6662 Lists NatList natlist ind
R6667:6673 Lists NatList natlist ind
R6686:6687 Lists <> l1 var
R6698:6700 Lists NatList nil constr
R6708:6709 Lists <> l2 var
R6716:6719 Lists NatList ::x_'::'_x not
R6726:6730 Lists NatList ::x_'::'_x not
R6739:6739 Lists NatList ::x_'::'_x not
R6731:6733 Lists <> app def
R6737:6738 Lists <> l2 var
R6903:6905 Lists NatList app def
not 6890:6890 NatList ::x_'++'_x
def 6978:6986 NatList test_app1
R7017:7019 Coq.Init.Logic <> :type_scope:x_'='_x not
R7008:7011 Lists NatList ::x_'++'_x not
R7001:7001 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7003:7003 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7005:7005 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7007:7007 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7012:7012 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7014:7014 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7016:7016 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7020:7020 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7022:7022 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7024:7024 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7026:7026 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7028:7028 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7030:7030 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 7067:7075 NatList test_app2
R7102:7104 Coq.Init.Logic <> :type_scope:x_'='_x not
R7093:7096 Lists NatList ::x_'++'_x not
R7090:7092 Lists NatList nil constr
R7097:7097 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7099:7099 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7101:7101 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7105:7105 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7107:7107 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7109:7109 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 7146:7154 NatList test_app3
R7183:7185 Coq.Init.Logic <> :type_scope:x_'='_x not
R7176:7179 Lists NatList ::x_'++'_x not
R7169:7169 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7171:7171 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7173:7173 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7175:7175 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7180:7182 Lists NatList nil constr
R7186:7186 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7188:7188 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7190:7190 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7192:7192 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 7677:7678 NatList hd
R7689:7691 Coq.Init.Datatypes <> nat ind
R7697:7703 Lists NatList natlist ind
R7708:7710 Coq.Init.Datatypes <> nat ind
R7723:7723 Lists <> l var
R7734:7736 Lists NatList nil constr
R7741:7747 Lists <> default var
R7754:7757 Lists NatList ::x_'::'_x not
def 7784:7785 NatList tl
R7790:7796 Lists NatList natlist ind
R7801:7807 Lists NatList natlist ind
R7820:7820 Lists <> l var
R7831:7833 Lists NatList nil constr
R7838:7840 Lists NatList nil constr
R7847:7850 Lists NatList ::x_'::'_x not
def 7874:7881 NatList test_hd1
R7908:7910 Coq.Init.Logic <> :type_scope:x_'='_x not
R7896:7897 Lists NatList hd def
R7901:7901 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7903:7903 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7905:7905 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R7907:7907 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 7948:7955 NatList test_hd2
R7977:7979 Coq.Init.Logic <> :type_scope:x_'='_x not
R7970:7971 Lists NatList hd def
R7975:7976 Lists NatList ::'['_']' not
def 8017:8023 NatList test_tl
R8049:8051 Coq.Init.Logic <> :type_scope:x_'='_x not
R8039:8040 Lists NatList tl def
R8042:8042 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8044:8044 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8046:8046 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8048:8048 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8052:8052 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8054:8054 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8056:8056 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 8415:8422 NatList nonzeros
R8427:8433 Lists NatList natlist ind
R8438:8444 Lists NatList natlist ind
R8457:8457 Lists <> l var
R8470:8471 Lists NatList ::'['_']' not
R8476:8477 Lists NatList ::'['_']' not
R8486:8489 Lists NatList ::x_'::'_x not
R8499:8505 Basics <> beq_nat def
R8534:8538 Lists NatList ::x_'::'_x not
R8550:8550 Lists NatList ::x_'::'_x not
R8539:8546 Lists <> nonzeros def
R8516:8523 Lists <> nonzeros def
def 8568:8580 NatList test_nonzeros
R8609:8611 Coq.Init.Logic <> :type_scope:x_'='_x not
R8585:8592 Lists NatList nonzeros def
R8594:8594 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8596:8596 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8598:8598 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8600:8600 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8602:8602 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8604:8604 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8606:8606 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8608:8608 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8612:8612 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8614:8614 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8616:8616 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8618:8618 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8701:8704 Basics <> oddb def
def 8716:8725 NatList oddmembers
R8730:8736 Lists NatList natlist ind
R8741:8747 Lists NatList natlist ind
R8762:8762 Lists <> l var
R8775:8776 Lists NatList ::'['_']' not
R8781:8782 Lists NatList ::'['_']' not
R8791:8794 Lists NatList ::x_'::'_x not
R8804:8807 Basics <> oddb def
R8842:8851 Lists <> oddmembers def
R8817:8821 Lists NatList ::x_'::'_x not
R8835:8835 Lists NatList ::x_'::'_x not
R8822:8831 Lists <> oddmembers def
def 8874:8888 NatList test_oddmembers
R8919:8921 Coq.Init.Logic <> :type_scope:x_'='_x not
R8893:8902 Lists NatList oddmembers def
R8904:8904 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8906:8906 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8908:8908 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8910:8910 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8912:8912 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8914:8914 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8916:8916 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8918:8918 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8922:8922 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8924:8924 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R8926:8926 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9014:9019 Lists NatList length def
R9021:9021 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9023:9023 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9025:9025 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9027:9027 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9029:9029 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 9044:9058 NatList countoddmembers
R9063:9069 Lists NatList natlist ind
R9074:9076 Coq.Init.Datatypes <> nat ind
R9083:9088 Lists NatList length def
R9091:9100 Lists NatList oddmembers def
R9102:9102 Lists <> l var
def 9115:9135 NatList test_countoddmembers1
R9169:9171 Coq.Init.Logic <> :type_scope:x_'='_x not
R9140:9154 Lists NatList countoddmembers def
R9156:9156 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9158:9158 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9160:9160 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9162:9162 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9164:9164 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9166:9166 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9168:9168 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 9211:9231 NatList test_countoddmembers2
R9259:9261 Coq.Init.Logic <> :type_scope:x_'='_x not
R9236:9250 Lists NatList countoddmembers def
R9252:9252 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9254:9254 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9256:9256 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R9258:9258 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 9301:9321 NatList test_countoddmembers3
R9345:9347 Coq.Init.Logic <> :type_scope:x_'='_x not
R9326:9340 Lists NatList countoddmembers def
R9342:9344 Lists NatList nil constr
def 10079:10087 NatList alternate
R10098:10104 Lists NatList natlist ind
R10109:10115 Lists NatList natlist ind
R10131:10132 Lists <> l1 var
R10147:10148 Lists NatList ::'['_']' not
R10153:10154 Lists <> l2 var
R10165:10168 Lists NatList ::x_'::'_x not
R10181:10182 Lists <> l2 var
R10213:10214 Lists NatList ::'['_']' not
R10219:10220 Lists <> l1 var
R10248:10251 Lists NatList ::x_'::'_x not
R10259:10261 Lists NatList app def
R10271:10279 Lists <> alternate def
R10263:10263 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10265:10265 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10268:10268 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 10332:10346 NatList test_alternate1
R10376:10378 Coq.Init.Logic <> :type_scope:x_'='_x not
R10351:10359 Lists NatList alternate def
R10369:10369 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10371:10371 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10373:10373 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10375:10375 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10361:10361 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10363:10363 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10365:10365 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10367:10367 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10379:10379 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10381:10381 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10383:10383 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10385:10385 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10387:10387 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10389:10389 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10391:10391 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 10430:10444 NatList test_alternate2
R10470:10472 Coq.Init.Logic <> :type_scope:x_'='_x not
R10449:10457 Lists NatList alternate def
R10463:10463 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10465:10465 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10467:10467 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10469:10469 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10459:10459 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10461:10461 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10473:10473 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10475:10475 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10477:10477 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10479:10479 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10481:10481 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 10520:10534 NatList test_alternate3
R10560:10562 Coq.Init.Logic <> :type_scope:x_'='_x not
R10539:10547 Lists NatList alternate def
R10557:10557 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10559:10559 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10549:10549 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10551:10551 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10553:10553 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10555:10555 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10563:10563 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10565:10565 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10567:10567 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10569:10569 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10571:10571 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 10610:10624 NatList test_alternate4
R10649:10651 Coq.Init.Logic <> :type_scope:x_'='_x not
R10629:10637 Lists NatList alternate def
R10642:10642 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10645:10645 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10648:10648 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10639:10640 Lists NatList ::'['_']' not
R10652:10652 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10655:10655 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R10658:10658 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 11001:11003 NatList bag
R11008:11014 Lists NatList natlist ind
def 11198:11202 NatList count
R11207:11209 Coq.Init.Datatypes <> nat ind
R11215:11217 Lists NatList bag def
R11222:11224 Coq.Init.Datatypes <> nat ind
R11239:11239 Lists <> s var
R11252:11253 Lists NatList ::'['_']' not
R11267:11270 Lists NatList ::x_'::'_x not
R11280:11286 Basics <> beq_nat def
R11290:11290 Lists <> v var
R11316:11320 Lists <> count def
R11322:11322 Lists <> v var
R11297:11297 Coq.Init.Datatypes <> S constr
R11299:11303 Lists <> count def
R11305:11305 Lists <> v var
def 11405:11415 NatList test_count1
R11452:11454 Coq.Init.Logic <> :type_scope:x_'='_x not
R11431:11435 Lists NatList count def
R11439:11439 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11441:11441 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11443:11443 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11445:11445 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11447:11447 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11449:11449 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11451:11451 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 11493:11503 NatList test_count2
R11540:11542 Coq.Init.Logic <> :type_scope:x_'='_x not
R11519:11523 Lists NatList count def
R11527:11527 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11529:11529 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11531:11531 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11533:11533 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11535:11535 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11537:11537 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R11539:11539 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 12377:12379 NatList sum
R12386:12389 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12393:12396 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12397:12399 Lists NatList bag def
R12390:12392 Lists NatList bag def
R12383:12385 Lists NatList bag def
R12404:12406 Lists NatList app def
def 12418:12426 NatList test_sum1
R12471:12473 Coq.Init.Logic <> :type_scope:x_'='_x not
R12442:12446 Lists NatList count def
R12451:12453 Lists NatList sum def
R12463:12463 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12465:12465 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12467:12467 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12469:12469 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12455:12455 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12457:12457 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12459:12459 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12461:12461 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 12557:12559 NatList add
R12564:12566 Coq.Init.Datatypes <> nat ind
R12572:12574 Lists NatList bag def
R12579:12581 Lists NatList bag def
R12586:12589 Lists NatList cons constr
R12593:12593 Lists <> s var
R12591:12591 Lists <> v var
def 12605:12613 NatList test_add1
R12654:12656 Coq.Init.Logic <> :type_scope:x_'='_x not
R12631:12635 Lists NatList count def
R12640:12642 Lists NatList add def
R12646:12646 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12648:12648 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12650:12650 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12652:12652 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 12693:12701 NatList test_add2
R12742:12744 Coq.Init.Logic <> :type_scope:x_'='_x not
R12719:12723 Lists NatList count def
R12728:12730 Lists NatList add def
R12734:12734 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12736:12736 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12738:12738 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R12740:12740 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 12871:12876 NatList member
R12881:12883 Coq.Init.Datatypes <> nat ind
R12889:12891 Lists NatList bag def
R12896:12899 Basics <> bool ind
R12913:12917 Lists NatList count def
R12921:12921 Lists <> s var
R12919:12919 Lists <> v var
R12935:12935 Coq.Init.Datatypes <> O constr
R12940:12944 Basics <> false constr
R12958:12961 Basics <> true constr
def 12979:12990 NatList test_member1
R13021:13023 Coq.Init.Logic <> :type_scope:x_'='_x not
R13005:13010 Lists NatList member def
R13014:13014 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13016:13016 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13018:13018 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13020:13020 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13024:13027 Basics <> true constr
def 13064:13075 NatList test_member2
R13106:13108 Coq.Init.Logic <> :type_scope:x_'='_x not
R13090:13095 Lists NatList member def
R13099:13099 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13101:13101 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13103:13103 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13105:13105 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13109:13113 Basics <> false constr
def 13414:13423 NatList remove_one
R13428:13430 Coq.Init.Datatypes <> nat ind
R13436:13438 Lists NatList bag def
R13443:13445 Lists NatList bag def
R13458:13458 Lists <> s var
R13471:13472 Lists NatList ::'['_']' not
R13477:13478 Lists NatList ::'['_']' not
R13487:13490 Lists NatList ::x_'::'_x not
R13500:13506 Basics <> beq_nat def
R13510:13510 Lists <> v var
R13526:13530 Lists NatList ::x_'::'_x not
R13546:13546 Lists NatList ::x_'::'_x not
R13531:13540 Lists <> remove_one def
R13542:13542 Lists <> v var
def 13564:13579 NatList test_remove_one1
R13618:13620 Coq.Init.Logic <> :type_scope:x_'='_x not
R13584:13588 Lists NatList count def
R13593:13602 Lists NatList remove_one def
R13606:13606 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13608:13608 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13610:13610 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13612:13612 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13614:13614 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13616:13616 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 13658:13673 NatList test_remove_one2
R13710:13712 Coq.Init.Logic <> :type_scope:x_'='_x not
R13678:13682 Lists NatList count def
R13687:13696 Lists NatList remove_one def
R13700:13700 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13702:13702 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13704:13704 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13706:13706 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13708:13708 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 13750:13765 NatList test_remove_one3
R13806:13808 Coq.Init.Logic <> :type_scope:x_'='_x not
R13770:13774 Lists NatList count def
R13779:13788 Lists NatList remove_one def
R13792:13792 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13794:13794 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13796:13796 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13798:13798 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13800:13800 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13802:13802 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13804:13804 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 13846:13861 NatList test_remove_one4
R13904:13906 Coq.Init.Logic <> :type_scope:x_'='_x not
R13866:13870 Lists NatList count def
R13875:13884 Lists NatList remove_one def
R13888:13888 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13890:13890 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13892:13892 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13894:13894 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13896:13896 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13898:13898 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13900:13900 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R13902:13902 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 13945:13954 NatList remove_all
R13959:13961 Coq.Init.Datatypes <> nat ind
R13967:13969 Lists NatList bag def
R13974:13976 Lists NatList bag def
R13989:13989 Lists <> s var
R14000:14001 Lists NatList ::'['_']' not
R14006:14007 Lists NatList ::'['_']' not
R14014:14017 Lists NatList ::x_'::'_x not
R14027:14033 Basics <> beq_nat def
R14037:14037 Lists <> v var
R14068:14072 Lists NatList ::x_'::'_x not
R14088:14088 Lists NatList ::x_'::'_x not
R14073:14082 Lists <> remove_all def
R14084:14084 Lists <> v var
R14045:14054 Lists <> remove_all def
R14056:14056 Lists <> v var
def 14106:14121 NatList test_remove_all1
R14159:14161 Coq.Init.Logic <> :type_scope:x_'='_x not
R14125:14129 Lists NatList count def
R14134:14143 Lists NatList remove_all def
R14147:14147 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14149:14149 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14151:14151 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14153:14153 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14155:14155 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14157:14157 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 14198:14213 NatList test_remove_all2
R14249:14251 Coq.Init.Logic <> :type_scope:x_'='_x not
R14217:14221 Lists NatList count def
R14226:14235 Lists NatList remove_all def
R14239:14239 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14241:14241 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14243:14243 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14245:14245 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14247:14247 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 14289:14304 NatList test_remove_all3
R14344:14346 Coq.Init.Logic <> :type_scope:x_'='_x not
R14308:14312 Lists NatList count def
R14317:14326 Lists NatList remove_all def
R14330:14330 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14332:14332 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14334:14334 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14336:14336 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14338:14338 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14340:14340 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14342:14342 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 14383:14398 NatList test_remove_all4
R14446:14448 Coq.Init.Logic <> :type_scope:x_'='_x not
R14402:14406 Lists NatList count def
R14411:14420 Lists NatList remove_all def
R14424:14424 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14426:14426 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14428:14428 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14430:14430 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14432:14432 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14434:14434 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14436:14436 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14438:14438 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14440:14440 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14442:14442 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14444:14444 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 14488:14493 NatList subset
R14499:14501 Lists NatList bag def
R14508:14510 Lists NatList bag def
R14515:14518 Basics <> bool ind
R14532:14533 Lists <> s1 var
R14546:14547 Lists NatList ::'['_']' not
R14552:14555 Basics <> true constr
R14564:14567 Lists NatList ::x_'::'_x not
R14577:14579 Basics <> leb def
R14595:14599 Lists NatList count def
R14603:14604 Lists <> s2 var
R14582:14586 Lists NatList count def
R14590:14591 Lists <> s1 var
R14686:14690 Basics <> false constr
R14634:14639 Lists <> subset def
R14645:14654 Lists NatList remove_one def
R14658:14659 Lists <> s2 var
def 14708:14719 NatList test_subset1
R14757:14759 Coq.Init.Logic <> :type_scope:x_'='_x not
R14735:14740 Lists NatList subset def
R14748:14748 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14750:14750 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14752:14752 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14754:14754 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14756:14756 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14742:14742 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14744:14744 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14746:14746 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14760:14763 Basics <> true constr
def 14800:14811 NatList test_subset2
R14851:14853 Coq.Init.Logic <> :type_scope:x_'='_x not
R14827:14832 Lists NatList subset def
R14842:14842 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14844:14844 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14846:14846 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14848:14848 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14850:14850 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14834:14834 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14836:14836 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14838:14838 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14840:14840 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R14854:14858 Basics <> false constr
prf 15724:15730 NatList nil_app
R15743:15749 Lists NatList natlist ind
R15761:15763 Coq.Init.Logic <> :type_scope:x_'='_x not
R15756:15759 Lists NatList ::x_'++'_x not
R15754:15755 Lists NatList ::'['_']' not
R15760:15760 Lists <> l var
R15764:15764 Lists <> l var
prf 16166:16179 NatList tl_length_pred
R16192:16198 Lists NatList natlist ind
R16218:16220 Coq.Init.Logic <> :type_scope:x_'='_x not
R16203:16206 Coq.Init.Peano <> pred syndef
R16209:16214 Lists NatList length def
R16216:16216 Lists <> l var
R16221:16226 Lists NatList length def
R16229:16230 Lists NatList tl def
R16232:16232 Lists <> l var
prf 18809:18817 NatList app_assoc
R18839:18845 Lists NatList natlist ind
R18866:18868 Coq.Init.Logic <> :type_scope:x_'='_x not
R18850:18850 Lists NatList ::x_'++'_x not
R18859:18863 Lists NatList ::x_'++'_x not
R18853:18856 Lists NatList ::x_'++'_x not
R18851:18852 Lists <> l1 var
R18857:18858 Lists <> l2 var
R18864:18865 Lists <> l3 var
R18871:18875 Lists NatList ::x_'++'_x not
R18884:18884 Lists NatList ::x_'++'_x not
R18869:18870 Lists <> l1 var
R18878:18881 Lists NatList ::x_'++'_x not
R18876:18877 Lists <> l2 var
R18882:18883 Lists <> l3 var
def 20861:20863 NatList rev
R20868:20874 Lists NatList natlist ind
R20879:20885 Lists NatList natlist ind
R20898:20898 Lists <> l var
R20909:20911 Lists NatList nil constr
R20919:20921 Lists NatList nil constr
R20928:20931 Lists NatList ::x_'::'_x not
R20942:20945 Lists NatList ::x_'++'_x not
R20937:20939 Lists <> rev def
R20946:20946 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R20948:20948 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 20966:20974 NatList test_rev1
R20999:21001 Coq.Init.Logic <> :type_scope:x_'='_x not
R20988:20990 Lists NatList rev def
R20992:20992 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R20994:20994 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R20996:20996 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R20998:20998 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R21002:21002 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R21004:21004 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R21006:21006 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R21008:21008 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
def 21045:21053 NatList test_rev2
R21074:21076 Coq.Init.Logic <> :type_scope:x_'='_x not
R21067:21069 Lists NatList rev def
R21071:21073 Lists NatList nil constr
R21077:21079 Lists NatList nil constr
prf 21478:21496 NatList rev_length_firsttry
R21511:21517 Lists NatList natlist ind
R21536:21538 Coq.Init.Logic <> :type_scope:x_'='_x not
R21522:21527 Lists NatList length def
R21530:21532 Lists NatList rev def
R21534:21534 Lists <> l var
R21539:21544 Lists NatList length def
R21546:21546 Lists <> l var
prf 22251:22260 NatList app_length
R22279:22285 Lists NatList natlist ind
R22307:22309 Coq.Init.Logic <> :type_scope:x_'='_x not
R22290:22295 Lists NatList length def
R22300:22303 Lists NatList ::x_'++'_x not
R22298:22299 Lists <> l1 var
R22304:22305 Lists <> l2 var
R22310:22310 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R22320:22324 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R22334:22334 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R22311:22316 Lists NatList length def
R22318:22319 Lists <> l1 var
R22325:22330 Lists NatList length def
R22332:22333 Lists <> l2 var
prf 22925:22934 NatList rev_length
R22949:22955 Lists NatList natlist ind
R22974:22976 Coq.Init.Logic <> :type_scope:x_'='_x not
R22960:22965 Lists NatList length def
R22968:22970 Lists NatList rev def
R22972:22972 Lists <> l var
R22977:22982 Lists NatList length def
R22984:22984 Lists <> l var
R23112:23121 Lists NatList app_length thm
R23124:23132 Induction <> plus_comm thm
R23112:23121 Lists NatList app_length thm
R23112:23121 Lists NatList app_length thm
R23124:23132 Induction <> plus_comm thm
R23124:23132 Induction <> plus_comm thm
prf 26811:26819 NatList app_nil_r
R26834:26840 Lists NatList natlist ind
R26852:26854 Coq.Init.Logic <> :type_scope:x_'='_x not
R26846:26849 Lists NatList ::x_'++'_x not
R26845:26845 Lists <> l var
R26850:26851 Lists NatList ::'['_']' not
R26855:26855 Lists <> l var
prf 26977:26989 NatList rev_app_distr
R27007:27013 Lists NatList natlist ind
R27032:27034 Coq.Init.Logic <> :type_scope:x_'='_x not
R27018:27020 Lists NatList rev def
R27025:27028 Lists NatList ::x_'++'_x not
R27023:27024 Lists <> l1 var
R27029:27030 Lists <> l2 var
R27041:27044 Lists NatList ::x_'++'_x not
R27035:27037 Lists NatList rev def
R27039:27040 Lists <> l2 var
R27045:27047 Lists NatList rev def
R27049:27050 Lists <> l1 var
R27127:27135 Lists NatList app_nil_r thm
R27127:27135 Lists NatList app_nil_r thm
R27127:27135 Lists NatList app_nil_r thm
R27186:27189 Lists NatList ::x_'++'_x not
R27191:27194 Lists NatList ::x_'++'_x not
R27207:27215 Lists NatList app_assoc thm
R27207:27215 Lists NatList app_assoc thm
R27207:27215 Lists NatList app_assoc thm
prf 27250:27263 NatList rev_involutive
R27278:27284 Lists NatList natlist ind
R27300:27302 Coq.Init.Logic <> :type_scope:x_'='_x not
R27289:27291 Lists NatList rev def
R27294:27296 Lists NatList rev def
R27298:27298 Lists <> l var
R27303:27303 Lists <> l var
R27392:27404 Lists NatList rev_app_distr thm
R27392:27404 Lists NatList rev_app_distr thm
R27392:27404 Lists NatList rev_app_distr thm
prf 27594:27603 NatList app_assoc4
R27628:27634 Lists NatList natlist ind
R27663:27665 Coq.Init.Logic <> :type_scope:x_'='_x not
R27641:27645 Lists NatList ::x_'++'_x not
R27662:27662 Lists NatList ::x_'++'_x not
R27639:27640 Lists <> l1 var
R27648:27652 Lists NatList ::x_'++'_x not
R27661:27661 Lists NatList ::x_'++'_x not
R27646:27647 Lists <> l2 var
R27655:27658 Lists NatList ::x_'++'_x not
R27653:27654 Lists <> l3 var
R27659:27660 Lists <> l4 var
R27666:27666 Lists NatList ::x_'++'_x not
R27683:27687 Lists NatList ::x_'++'_x not
R27667:27667 Lists NatList ::x_'++'_x not
R27676:27680 Lists NatList ::x_'++'_x not
R27670:27673 Lists NatList ::x_'++'_x not
R27668:27669 Lists <> l1 var
R27674:27675 Lists <> l2 var
R27681:27682 Lists <> l3 var
R27688:27689 Lists <> l4 var
R27773:27781 Lists NatList app_assoc thm
R27773:27781 Lists NatList app_assoc thm
R27773:27781 Lists NatList app_assoc thm
prf 27908:27919 NatList nonzeros_app
R27938:27944 Lists NatList natlist ind
R27968:27970 Coq.Init.Logic <> :type_scope:x_'='_x not
R27949:27956 Lists NatList nonzeros def
R27961:27964 Lists NatList ::x_'++'_x not
R27959:27960 Lists <> l1 var
R27965:27966 Lists <> l2 var
R27971:27971 Lists NatList ::x_'++'_x not
R27983:27988 Lists NatList ::x_'++'_x not
R28000:28000 Lists NatList ::x_'++'_x not
R27972:27979 Lists NatList nonzeros def
R27981:27982 Lists <> l1 var
R27989:27996 Lists NatList nonzeros def
R27998:27999 Lists <> l2 var
R28098:28104 Basics <> beq_nat def
R28098:28104 Basics <> beq_nat def
def 28415:28425 NatList beq_natlist
R28436:28442 Lists NatList natlist ind
R28447:28450 Basics <> bool ind
R28463:28464 Lists <> l1 var
R28477:28479 Lists NatList nil constr
R28490:28491 Lists <> l2 var
R28517:28519 Lists NatList nil constr
R28524:28527 Basics <> true constr
R28553:28557 Basics <> false constr
R28586:28587 Lists NatList ::x_'::'_x not
R28601:28602 Lists <> l2 var
R28631:28633 Lists NatList nil constr
R28638:28642 Basics <> false constr
R28668:28669 Lists NatList ::x_'::'_x not
R28680:28686 Basics <> beq_nat def
R28724:28728 Basics <> false constr
R28699:28709 Lists <> beq_natlist def
def 28771:28787 NatList test_beq_natlist1
R28813:28815 Coq.Init.Logic <> :type_scope:x_'='_x not
R28794:28804 Lists NatList beq_natlist def
R28810:28812 Lists NatList nil constr
R28806:28808 Lists NatList nil constr
R28816:28819 Basics <> true constr
def 28858:28874 NatList test_beq_natlist2
R28907:28909 Coq.Init.Logic <> :type_scope:x_'='_x not
R28880:28890 Lists NatList beq_natlist def
R28900:28900 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28902:28902 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28904:28904 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28906:28906 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28892:28892 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28894:28894 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28896:28896 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28898:28898 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28910:28913 Basics <> true constr
def 28950:28966 NatList test_beq_natlist3
R28999:29001 Coq.Init.Logic <> :type_scope:x_'='_x not
R28972:28982 Lists NatList beq_natlist def
R28992:28992 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28994:28994 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28996:28996 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28998:28998 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28984:28984 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28986:28986 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28988:28988 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R28990:28990 Lists NatList ::'['_x_';'_'..'_';'_x_']' not
R29002:29006 Basics <> false constr
prf 29043:29058 NatList beq_natlist_refl
R29071:29077 Lists NatList natlist ind
R29086:29088 Coq.Init.Logic <> :type_scope:x_'='_x not
R29082:29085 Basics <> true constr
R29089:29099 Lists NatList beq_natlist def
R29103:29103 Lists <> l var
R29101:29101 Lists <> l var
R29198:29204 Basics <> beq_nat def
R29198:29204 Basics <> beq_nat def
R29268:29274 Basics <> beq_nat def
R29283:29294 Induction <> beq_nat_refl thm
R29283:29294 Induction <> beq_nat_refl thm
prf 29579:29598 NatList count_member_nonzero
R29614:29616 Lists NatList bag def
R29646:29648 Coq.Init.Logic <> :type_scope:x_'='_x not
R29622:29624 Basics <> leb def
R29629:29633 Lists NatList count def
R29639:29642 Lists NatList ::x_'::'_x not
R29643:29643 Lists <> s var
R29649:29652 Basics <> true constr
prf 29790:29797 NatList ble_n_Sn
R29824:29826 Coq.Init.Logic <> :type_scope:x_'='_x not
R29813:29815 Basics <> leb def
R29820:29820 Coq.Init.Datatypes <> S constr
R29822:29822 Lists <> n var
R29817:29817 Lists <> n var
R29827:29830 Basics <> true constr
prf 30053:30074 NatList remove_decreases_count
R30089:30091 Lists NatList bag def
R30139:30141 Coq.Init.Logic <> :type_scope:x_'='_x not
R30097:30099 Basics <> leb def
R30129:30133 Lists NatList count def
R30137:30137 Lists <> s var
R30102:30106 Lists NatList count def
R30111:30120 Lists NatList remove_one def
R30124:30124 Lists <> s var
R30142:30145 Basics <> true constr
R30236:30242 Basics <> beq_nat def
R30236:30242 Basics <> beq_nat def
R30270:30277 Lists NatList ble_n_Sn thm
R30270:30277 Lists NatList ble_n_Sn thm
prf 30719:30731 NatList rev_injective
R30748:30754 Lists NatList natlist ind
R30772:30775 Coq.Init.Logic <> :type_scope:x_'->'_x not
R30778:30780 Coq.Init.Logic <> :type_scope:x_'='_x not
R30776:30777 Lists <> l1 var
R30781:30782 Lists <> l2 var
R30763:30765 Coq.Init.Logic <> :type_scope:x_'='_x not
R30757:30759 Lists NatList rev def
R30761:30762 Lists <> l1 var
R30766:30768 Lists NatList rev def
R30770:30771 Lists <> l2 var
R30821:30823 Lists NatList rev def
R30837:30850 Lists NatList rev_involutive thm
R30837:30850 Lists NatList rev_involutive thm
R30837:30850 Lists NatList rev_involutive thm
R30875:30888 Lists NatList rev_involutive thm
R30875:30888 Lists NatList rev_involutive thm
R30875:30888 Lists NatList rev_involutive thm
prf 30921:30935 NatList rev_injective_l
R30951:30957 Lists NatList natlist ind
R30967:30970 Coq.Init.Logic <> :type_scope:x_'->'_x not
R30977:30979 Coq.Init.Logic <> :type_scope:x_'='_x not
R30971:30973 Lists NatList rev def
R30975:30976 Lists <> l1 var
R30980:30982 Lists NatList rev def
R30984:30985 Lists <> l2 var
R30962:30964 Coq.Init.Logic <> :type_scope:x_'='_x not
R30960:30961 Lists <> l1 var
R30965:30966 Lists <> l2 var
prf 31056:31069 NatList rev_injective'
R31086:31092 Lists NatList natlist ind
R31110:31113 Coq.Init.Logic <> :type_scope:x_'->'_x not
R31116:31118 Coq.Init.Logic <> :type_scope:x_'='_x not
R31114:31115 Lists <> l1 var
R31119:31120 Lists <> l2 var
R31101:31103 Coq.Init.Logic <> :type_scope:x_'='_x not
R31095:31097 Lists NatList rev def
R31099:31100 Lists <> l1 var
R31104:31106 Lists NatList rev def
R31108:31109 Lists <> l2 var
R31197:31199 Lists NatList rev def
R31221:31223 Lists NatList rev def
R31237:31250 Lists NatList rev_involutive thm
R31237:31250 Lists NatList rev_involutive thm
R31237:31250 Lists NatList rev_involutive thm
R31309:31322 Lists NatList rev_involutive thm
R31309:31322 Lists NatList rev_involutive thm
R31309:31322 Lists NatList rev_involutive thm
R31347:31360 Lists NatList rev_involutive thm
R31347:31360 Lists NatList rev_involutive thm
R31347:31360 Lists NatList rev_involutive thm
def 31914:31920 NatList nth_bad