-
Notifications
You must be signed in to change notification settings - Fork 0
/
c5.glob
1321 lines (1321 loc) · 52.9 KB
/
c5.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 f0ae3eb2536b3c6418ed2864ab3f2af2
Fc5
R24:26 Coq.Init.Nat <> <> lib
R54:57 Coq.Lists.List <> <> lib
R78:80 Coq.Init.Datatypes <> nil constr
not 69:69 <> ::list_scope:'['_']'
R132:135 Coq.Init.Datatypes <> cons constr
R139:141 Coq.Init.Datatypes <> nil constr
not 120:120 <> ::list_scope:'['_x_']'
R192:195 Coq.Init.Datatypes <> cons constr
R200:203 Coq.Init.Datatypes <> cons constr
R211:214 Coq.Init.Datatypes <> cons constr
R218:220 Coq.Init.Datatypes <> nil constr
not 167:167 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']'
R300:300 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R302:302 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R304:304 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
prf 317:322 <> silly1
R340:342 Coq.Init.Datatypes <> nat ind
binder 334:334 <> n:1
binder 336:336 <> m:2
R355:358 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R351:353 Coq.Init.Logic <> ::type_scope:x_'='_x not
R350:350 c5 <> n:1 var
R354:354 c5 <> m:2 var
R360:362 Coq.Init.Logic <> ::type_scope:x_'='_x not
R359:359 c5 <> n:1 var
R363:363 c5 <> m:2 var
prf 472:477 <> silly2
R499:501 Coq.Init.Datatypes <> nat ind
binder 489:489 <> n:3
binder 491:491 <> m:4
binder 493:493 <> o:5
binder 495:495 <> p:6
R510:513 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R506:508 Coq.Init.Logic <> ::type_scope:x_'='_x not
R505:505 c5 <> n:3 var
R509:509 c5 <> m:4 var
R514:514 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R537:541 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R520:523 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R516:518 Coq.Init.Logic <> ::type_scope:x_'='_x not
R515:515 c5 <> n:3 var
R519:519 c5 <> m:4 var
R529:531 Coq.Init.Logic <> ::type_scope:x_'='_x not
R524:524 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R526:526 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R528:528 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R525:525 c5 <> n:3 var
R527:527 c5 <> o:5 var
R532:532 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R534:534 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R536:536 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R533:533 c5 <> m:4 var
R535:535 c5 <> p:6 var
R547:549 Coq.Init.Logic <> ::type_scope:x_'='_x not
R542:542 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R544:544 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R546:546 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R543:543 c5 <> n:3 var
R545:545 c5 <> o:5 var
R550:550 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R552:552 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R554:554 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R551:551 c5 <> m:4 var
R553:553 c5 <> p:6 var
prf 635:641 <> silly2a
R659:661 Coq.Init.Datatypes <> nat ind
binder 653:653 <> n:7
binder 655:655 <> m:8
R680:685 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R672:674 Coq.Init.Logic <> ::type_scope:x_'='_x not
R667:667 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R669:669 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R671:671 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R668:668 c5 <> n:7 var
R670:670 c5 <> n:7 var
R675:675 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R677:677 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R679:679 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R676:676 c5 <> m:8 var
R678:678 c5 <> m:8 var
R686:686 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R733:739 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R701:703 Coq.Init.Datatypes <> nat ind
binder 695:695 <> q:9
binder 697:697 <> r:10
R720:723 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R712:714 Coq.Init.Logic <> ::type_scope:x_'='_x not
R707:707 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R709:709 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R711:711 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R708:708 c5 <> q:9 var
R710:710 c5 <> q:9 var
R715:715 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R717:717 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R719:719 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R716:716 c5 <> r:10 var
R718:718 c5 <> r:10 var
R727:729 Coq.Init.Logic <> ::type_scope:x_'='_x not
R724:724 c5 <> ::list_scope:'['_x_']' not
R726:726 c5 <> ::list_scope:'['_x_']' not
R725:725 c5 <> q:9 var
R730:730 c5 <> ::list_scope:'['_x_']' not
R732:732 c5 <> ::list_scope:'['_x_']' not
R731:731 c5 <> r:10 var
R743:745 Coq.Init.Logic <> ::type_scope:x_'='_x not
R740:740 c5 <> ::list_scope:'['_x_']' not
R742:742 c5 <> ::list_scope:'['_x_']' not
R741:741 c5 <> n:7 var
R746:746 c5 <> ::list_scope:'['_x_']' not
R748:748 c5 <> ::list_scope:'['_x_']' not
R747:747 c5 <> m:8 var
prf 950:957 <> silly2a'
R975:977 Coq.Init.Datatypes <> nat ind
binder 969:969 <> n:11
binder 971:971 <> m:12
R996:1001 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R988:990 Coq.Init.Logic <> ::type_scope:x_'='_x not
R983:983 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R985:985 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R987:987 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R984:984 c5 <> n:11 var
R986:986 c5 <> n:11 var
R991:991 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R993:993 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R995:995 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R992:992 c5 <> m:12 var
R994:994 c5 <> m:12 var
R1002:1002 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1049:1055 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1017:1019 Coq.Init.Datatypes <> nat ind
binder 1011:1011 <> q:13
binder 1013:1013 <> r:14
R1036:1039 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1028:1030 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1023:1023 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1025:1025 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1027:1027 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1024:1024 c5 <> q:13 var
R1026:1026 c5 <> q:13 var
R1031:1031 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1033:1033 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1035:1035 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1032:1032 c5 <> r:14 var
R1034:1034 c5 <> r:14 var
R1043:1045 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1040:1040 c5 <> ::list_scope:'['_x_']' not
R1042:1042 c5 <> ::list_scope:'['_x_']' not
R1041:1041 c5 <> q:13 var
R1046:1046 c5 <> ::list_scope:'['_x_']' not
R1048:1048 c5 <> ::list_scope:'['_x_']' not
R1047:1047 c5 <> r:14 var
R1059:1061 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1056:1056 c5 <> ::list_scope:'['_x_']' not
R1058:1058 c5 <> ::list_scope:'['_x_']' not
R1057:1057 c5 <> n:11 var
R1062:1062 c5 <> ::list_scope:'['_x_']' not
R1064:1064 c5 <> ::list_scope:'['_x_']' not
R1063:1063 c5 <> m:12 var
prf 1138:1145 <> silly_ex
binder 1156:1156 <> p:15
R1161:1161 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1207:1213 Coq.Init.Logic <> ::type_scope:x_'->'_x not
binder 1169:1169 <> n:16
R1185:1188 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1178:1180 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1172:1175 Coq.Init.Nat <> even def
R1177:1177 c5 <> n:16 var
R1181:1184 Coq.Init.Datatypes <> true constr
R1199:1201 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1189:1192 Coq.Init.Nat <> even def
R1195:1195 Coq.Init.Datatypes <> S constr
R1197:1197 c5 <> n:16 var
R1202:1206 Coq.Init.Datatypes <> false constr
R1214:1214 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1255:1261 Coq.Init.Logic <> ::type_scope:x_'->'_x not
binder 1222:1222 <> n:17
R1239:1242 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1231:1233 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1225:1228 Coq.Init.Nat <> even def
R1230:1230 c5 <> n:17 var
R1234:1238 Coq.Init.Datatypes <> false constr
R1248:1250 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1243:1245 Coq.Init.Nat <> odd def
R1247:1247 c5 <> n:17 var
R1251:1254 Coq.Init.Datatypes <> true constr
R1275:1280 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1268:1270 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1262:1265 Coq.Init.Nat <> even def
R1267:1267 c5 <> p:15 var
R1271:1274 Coq.Init.Datatypes <> true constr
R1290:1292 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1281:1283 Coq.Init.Nat <> odd def
R1286:1286 Coq.Init.Datatypes <> S constr
R1288:1288 c5 <> p:15 var
R1293:1296 Coq.Init.Datatypes <> true constr
prf 1448:1453 <> silly3
R1471:1473 Coq.Init.Datatypes <> nat ind
binder 1465:1465 <> n:18
binder 1467:1467 <> m:19
R1486:1489 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1482:1484 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1481:1481 c5 <> n:18 var
R1485:1485 c5 <> m:19 var
R1491:1493 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1490:1490 c5 <> m:19 var
R1494:1494 c5 <> n:18 var
R1580:1582 Coq.Lists.List <> rev def
R1585:1587 Coq.Lists.List <> rev def
prf 1601:1613 <> rev_exercise1
R1632:1635 Coq.Init.Datatypes <> list ind
R1637:1639 Coq.Init.Datatypes <> nat ind
binder 1625:1625 <> l:20
binder 1627:1628 <> l':21
R1655:1660 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1646:1648 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1645:1645 c5 <> l:20 var
R1649:1651 Coq.Lists.List <> rev def
R1653:1654 c5 <> l':21 var
R1663:1665 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1661:1662 c5 <> l':21 var
R1666:1668 Coq.Lists.List <> rev def
R1670:1670 c5 <> l:20 var
R1735:1748 Coq.Lists.List <> rev_involutive thm
R1735:1748 Coq.Lists.List <> rev_involutive thm
def 1824:1839 <> trans_eq_example
R1865:1867 Coq.Init.Datatypes <> nat ind
binder 1851:1851 <> a:22
binder 1853:1853 <> b:23
binder 1855:1855 <> c:24
binder 1857:1857 <> d:25
binder 1859:1859 <> e:26
binder 1861:1861 <> f:27
R1889:1897 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1881:1883 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1876:1876 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1878:1878 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1880:1880 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1877:1877 c5 <> a:22 var
R1879:1879 c5 <> b:23 var
R1884:1884 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1886:1886 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1888:1888 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1885:1885 c5 <> c:24 var
R1887:1887 c5 <> d:25 var
R1911:1919 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R1903:1905 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1898:1898 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1900:1900 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1902:1902 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1899:1899 c5 <> c:24 var
R1901:1901 c5 <> d:25 var
R1906:1906 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1908:1908 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1910:1910 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1907:1907 c5 <> e:26 var
R1909:1909 c5 <> f:27 var
R1925:1927 Coq.Init.Logic <> ::type_scope:x_'='_x not
R1920:1920 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1922:1922 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1924:1924 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1921:1921 c5 <> a:22 var
R1923:1923 c5 <> b:23 var
R1928:1928 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1930:1930 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1932:1932 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R1929:1929 c5 <> e:26 var
R1931:1931 c5 <> f:27 var
prf 2018:2025 <> trans_eq
binder 2037:2037 <> X:28
R2054:2054 c5 <> X:28 var
binder 2047:2047 <> n:29
binder 2049:2049 <> m:30
binder 2051:2051 <> o:31
R2065:2068 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2061:2063 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2060:2060 c5 <> n:29 var
R2064:2064 c5 <> m:30 var
R2074:2077 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2070:2072 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2069:2069 c5 <> m:30 var
R2073:2073 c5 <> o:31 var
R2079:2081 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2078:2078 c5 <> n:29 var
R2082:2082 c5 <> o:31 var
def 2174:2190 <> trans_eq_example'
R2216:2218 Coq.Init.Datatypes <> nat ind
binder 2202:2202 <> a:32
binder 2204:2204 <> b:33
binder 2206:2206 <> c:34
binder 2208:2208 <> d:35
binder 2210:2210 <> e:36
binder 2212:2212 <> f:37
R2240:2248 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2232:2234 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2227:2227 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2229:2229 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2231:2231 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2228:2228 c5 <> a:32 var
R2230:2230 c5 <> b:33 var
R2235:2235 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2237:2237 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2239:2239 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2236:2236 c5 <> c:34 var
R2238:2238 c5 <> d:35 var
R2262:2270 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2254:2256 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2249:2249 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2251:2251 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2253:2253 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2250:2250 c5 <> c:34 var
R2252:2252 c5 <> d:35 var
R2257:2257 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2259:2259 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2261:2261 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2258:2258 c5 <> e:36 var
R2260:2260 c5 <> f:37 var
R2276:2278 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2271:2271 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2273:2273 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2275:2275 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2272:2272 c5 <> a:32 var
R2274:2274 c5 <> b:33 var
R2279:2279 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2281:2281 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2283:2283 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2280:2280 c5 <> e:36 var
R2282:2282 c5 <> f:37 var
R2422:2422 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2424:2424 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2426:2426 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2422:2422 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2424:2424 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R2426:2426 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
def 2465:2472 <> minustwo
R2477:2479 Coq.Init.Datatypes <> nat ind
binder 2475:2475 <> n:38
R2483:2485 Coq.Init.Datatypes <> nat ind
R2497:2497 c5 <> n:38 var
R2508:2508 Coq.Init.Datatypes <> O constr
R2513:2513 Coq.Init.Datatypes <> O constr
R2519:2519 Coq.Init.Datatypes <> S constr
R2521:2521 Coq.Init.Datatypes <> O constr
R2526:2526 Coq.Init.Datatypes <> O constr
R2532:2532 Coq.Init.Datatypes <> S constr
R2534:2534 Coq.Init.Datatypes <> S constr
R2542:2549 c5 <> minustwo:39 def
def 2569:2585 <> trans_eq_exercise
R2607:2609 Coq.Init.Datatypes <> nat ind
binder 2597:2597 <> n:41
binder 2599:2599 <> m:42
binder 2601:2601 <> o:43
binder 2603:2603 <> p:44
R2634:2642 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2619:2622 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2633:2633 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2618:2618 c5 <> m:42 var
R2623:2630 c5 <> minustwo def
R2632:2632 c5 <> o:43 var
R2654:2662 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2643:2643 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2649:2652 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2645:2647 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R2644:2644 c5 <> n:41 var
R2648:2648 c5 <> p:44 var
R2653:2653 c5 <> m:42 var
R2663:2663 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2669:2673 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2684:2684 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2665:2667 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R2664:2664 c5 <> n:41 var
R2668:2668 c5 <> p:44 var
R2674:2681 c5 <> minustwo def
R2683:2683 c5 <> o:43 var
prf 2797:2807 <> S_injective
R2825:2827 Coq.Init.Datatypes <> nat ind
binder 2819:2819 <> n:45
binder 2821:2821 <> m:46
R2842:2847 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2836:2838 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2833:2833 Coq.Init.Datatypes <> S constr
R2835:2835 c5 <> n:45 var
R2839:2839 Coq.Init.Datatypes <> S constr
R2841:2841 c5 <> m:46 var
R2849:2851 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2848:2848 c5 <> n:45 var
R2852:2852 c5 <> m:46 var
R2905:2907 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2908:2911 Coq.Init.Nat <> pred def
R2913:2913 Coq.Init.Datatypes <> S constr
R2905:2907 Coq.Init.Logic <> ::type_scope:x_'='_x not
R2908:2911 Coq.Init.Nat <> pred def
R2913:2913 Coq.Init.Datatypes <> S constr
prf 2994:3005 <> S_injective'
R3023:3025 Coq.Init.Datatypes <> nat ind
binder 3017:3017 <> n:47
binder 3019:3019 <> m:48
R3040:3045 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3034:3036 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3031:3031 Coq.Init.Datatypes <> S constr
R3033:3033 c5 <> n:47 var
R3037:3037 Coq.Init.Datatypes <> S constr
R3039:3039 c5 <> m:48 var
R3047:3049 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3046:3046 c5 <> n:47 var
R3050:3050 c5 <> m:48 var
prf 3130:3142 <> injection_ex1
R3162:3164 Coq.Init.Datatypes <> nat ind
binder 3154:3154 <> n:49
binder 3156:3156 <> m:50
binder 3158:3158 <> o:51
R3183:3188 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3175:3177 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3170:3170 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R3172:3172 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R3174:3174 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R3171:3171 c5 <> n:49 var
R3173:3173 c5 <> m:50 var
R3178:3178 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R3180:3180 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R3182:3182 c5 <> ::list_scope:'['_x_';'_x_';'_'..'_';'_x_']' not
R3179:3179 c5 <> o:51 var
R3181:3181 c5 <> o:51 var
R3190:3192 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3189:3189 c5 <> n:49 var
R3193:3193 c5 <> m:50 var
def 3319:3331 <> injection_ex3
binder 3343:3343 <> X:52
R3362:3362 c5 <> X:52 var
binder 3354:3354 <> x:53
binder 3356:3356 <> y:54
binder 3358:3358 <> z:55
R3372:3375 Coq.Init.Datatypes <> list ind
R3377:3377 c5 <> X:52 var
binder 3366:3366 <> l:56
binder 3368:3368 <> j:57
R3403:3408 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3394:3396 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3384:3387 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3383:3383 c5 <> x:53 var
R3389:3392 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3388:3388 c5 <> y:54 var
R3393:3393 c5 <> l:56 var
R3398:3401 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3397:3397 c5 <> z:55 var
R3402:3402 c5 <> j:57 var
R3419:3424 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3410:3412 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3409:3409 c5 <> j:57 var
R3414:3417 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3413:3413 c5 <> z:55 var
R3418:3418 c5 <> l:56 var
R3426:3428 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3425:3425 c5 <> x:53 var
R3429:3429 c5 <> y:54 var
R3533:3536 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3528:3531 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3538:3541 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3533:3536 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3528:3531 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3538:3541 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
prf 3671:3686 <> discriminate_ex1
R3704:3706 Coq.Init.Datatypes <> nat ind
binder 3698:3698 <> n:58
binder 3700:3700 <> m:59
R3724:3729 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3717:3719 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3712:3716 Coq.Init.Datatypes <> false constr
R3720:3723 Coq.Init.Datatypes <> true constr
R3731:3733 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3730:3730 c5 <> n:58 var
R3734:3734 c5 <> m:59 var
prf 3799:3814 <> discriminate_ex2
R3830:3832 Coq.Init.Datatypes <> nat ind
binder 3826:3826 <> n:60
R3845:3850 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3841:3843 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3838:3838 Coq.Init.Datatypes <> S constr
R3840:3840 c5 <> n:60 var
R3844:3844 Coq.Init.Datatypes <> O constr
R3856:3858 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3852:3854 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
def 3923:3938 <> discriminate_ex3
binder 3952:3952 <> X:61
R3971:3971 c5 <> X:61 var
binder 3963:3963 <> x:62
binder 3965:3965 <> y:63
binder 3967:3967 <> z:64
R3981:3984 Coq.Init.Datatypes <> list ind
R3986:3986 c5 <> X:61 var
binder 3975:3975 <> l:65
binder 3977:3977 <> j:66
R4010:4017 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4005:4007 Coq.Init.Logic <> ::type_scope:x_'='_x not
R3995:3998 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3994:3994 c5 <> x:62 var
R4000:4003 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3999:3999 c5 <> y:63 var
R4004:4004 c5 <> l:65 var
R4008:4009 c5 <> ::list_scope:'['_']' not
R4019:4021 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4018:4018 c5 <> x:62 var
R4022:4022 c5 <> z:64 var
prf 4111:4117 <> eqb_0_l
binder 4128:4128 <> n:67
R4147:4150 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4140:4142 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4135:4138 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R4139:4139 c5 <> n:67 var
R4143:4146 Coq.Init.Datatypes <> true constr
R4152:4154 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4151:4151 c5 <> n:67 var
prf 4263:4269 <> f_equal
binder 4281:4281 <> A:68
binder 4283:4283 <> B:69
R4298:4301 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4297:4297 c5 <> A:68 var
R4302:4302 c5 <> B:69 var
binder 4294:4294 <> f:70
R4311:4311 c5 <> A:68 var
binder 4306:4306 <> x:71
binder 4308:4308 <> y:72
R4322:4325 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4318:4320 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4317:4317 c5 <> x:71 var
R4321:4321 c5 <> y:72 var
R4329:4331 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4326:4326 c5 <> f:70 var
R4328:4328 c5 <> x:71 var
R4332:4332 c5 <> f:70 var
R4334:4334 c5 <> y:72 var
prf 4403:4423 <> eq_implies_succ_equal
R4441:4443 Coq.Init.Datatypes <> nat ind
binder 4435:4435 <> n:73
binder 4437:4437 <> m:74
R4454:4457 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4450:4452 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4449:4449 c5 <> n:73 var
R4453:4453 c5 <> m:74 var
R4461:4463 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4458:4458 Coq.Init.Datatypes <> S constr
R4460:4460 c5 <> n:73 var
R4464:4464 Coq.Init.Datatypes <> S constr
R4466:4466 c5 <> m:74 var
R4496:4502 c5 <> f_equal thm
R4496:4502 c5 <> f_equal thm
prf 4528:4549 <> eq_implies_succ_equal'
R4567:4569 Coq.Init.Datatypes <> nat ind
binder 4561:4561 <> n:75
binder 4563:4563 <> m:76
R4580:4583 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4576:4578 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4575:4575 c5 <> n:75 var
R4579:4579 c5 <> m:76 var
R4587:4589 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4584:4584 Coq.Init.Datatypes <> S constr
R4586:4586 c5 <> n:75 var
R4590:4590 Coq.Init.Datatypes <> S constr
R4592:4592 c5 <> m:76 var
prf 4703:4707 <> S_inj
R4725:4727 Coq.Init.Datatypes <> nat ind
binder 4719:4719 <> n:77
binder 4721:4721 <> m:78
R4735:4738 Coq.Init.Datatypes <> bool ind
binder 4731:4731 <> b:79
R4764:4769 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4744:4744 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4759:4762 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4745:4745 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R4749:4754 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R4758:4758 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R4746:4746 Coq.Init.Datatypes <> S constr
R4748:4748 c5 <> n:77 var
R4755:4755 Coq.Init.Datatypes <> S constr
R4757:4757 c5 <> m:78 var
R4763:4763 c5 <> b:79 var
R4770:4770 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4777:4780 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4772:4775 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R4771:4771 c5 <> n:77 var
R4776:4776 c5 <> m:78 var
R4781:4781 c5 <> b:79 var
prf 4861:4866 <> silly4
R4888:4890 Coq.Init.Datatypes <> nat ind
binder 4878:4878 <> n:80
binder 4880:4880 <> m:81
binder 4882:4882 <> p:82
binder 4884:4884 <> q:83
R4896:4896 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4911:4917 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4902:4905 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4898:4900 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4897:4897 c5 <> n:80 var
R4901:4901 c5 <> m:81 var
R4907:4909 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4906:4906 c5 <> p:82 var
R4910:4910 c5 <> q:83 var
R4923:4928 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4919:4921 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4918:4918 c5 <> m:81 var
R4922:4922 c5 <> n:80 var
R4930:4932 Coq.Init.Logic <> ::type_scope:x_'='_x not
R4929:4929 c5 <> q:83 var
R4933:4933 c5 <> p:82 var
prf 5099:5106 <> eqb_true
binder 5117:5117 <> n:84
binder 5119:5119 <> m:85
R5137:5140 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5130:5132 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5125:5128 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R5124:5124 c5 <> n:84 var
R5129:5129 c5 <> m:85 var
R5133:5136 Coq.Init.Datatypes <> true constr
R5142:5144 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5141:5141 c5 <> n:84 var
R5145:5145 c5 <> m:85 var
R5384:5404 c5 <> eq_implies_succ_equal thm
R5384:5404 c5 <> eq_implies_succ_equal thm
R5430:5438 Coq.Init.Peano <> plus_n_Sm thm
prf 5449:5466 <> plus_n_n_injective
binder 5477:5477 <> n:86
binder 5479:5479 <> m:87
R5497:5502 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5489:5491 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5485:5487 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R5484:5484 c5 <> n:86 var
R5488:5488 c5 <> n:86 var
R5493:5495 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R5492:5492 c5 <> m:87 var
R5496:5496 c5 <> m:87 var
R5504:5506 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5503:5503 c5 <> n:86 var
R5507:5507 c5 <> m:87 var
R5748:5756 Coq.Init.Peano <> plus_n_Sm thm
R5748:5756 Coq.Init.Peano <> plus_n_Sm thm
R5748:5756 Coq.Init.Peano <> plus_n_Sm thm
R5775:5783 Coq.Init.Peano <> plus_n_Sm thm
R5775:5783 Coq.Init.Peano <> plus_n_Sm thm
R5775:5783 Coq.Init.Peano <> plus_n_Sm thm
R5842:5862 c5 <> eq_implies_succ_equal thm
R5842:5862 c5 <> eq_implies_succ_equal thm
R5886:5891 Coq.Init.Nat <> double def
R5893:5895 Coq.Init.Datatypes <> nat ind
R5904:5909 Coq.Init.Nat <> double def
prf 5940:5947 <> double_S
R5959:5961 Coq.Init.Datatypes <> nat ind
binder 5957:5957 <> n:88
R5979:5980 Coq.Init.Logic <> ::type_scope:x_'='_x not
R5966:5971 Coq.Init.Nat <> double def
R5974:5974 Coq.Init.Datatypes <> S constr
R5976:5976 c5 <> n:88 var
R5981:5981 Coq.Init.Datatypes <> S constr
R5983:5983 Coq.Init.Datatypes <> S constr
R5985:5990 Coq.Init.Nat <> double def
R5992:5992 c5 <> n:88 var
R6056:6061 Coq.Init.Nat <> double def
R6082:6090 Coq.Init.Peano <> plus_n_Sm thm
R6082:6090 Coq.Init.Peano <> plus_n_Sm thm
R6082:6090 Coq.Init.Peano <> plus_n_Sm thm
prf 6120:6141 <> double_injective_take2
binder 6152:6152 <> n:89
binder 6154:6154 <> m:90
R6178:6183 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6167:6169 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6159:6164 Coq.Init.Nat <> double def
R6166:6166 c5 <> n:89 var
R6170:6175 Coq.Init.Nat <> double def
R6177:6177 c5 <> m:90 var
R6185:6187 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6184:6184 c5 <> n:89 var
R6188:6188 c5 <> m:90 var
R6666:6672 c5 <> f_equal thm
R6666:6672 c5 <> f_equal thm
R6701:6708 c5 <> double_S thm
R6701:6708 c5 <> double_S thm
R6701:6708 c5 <> double_S thm
R6725:6732 c5 <> double_S thm
R6725:6732 c5 <> double_S thm
R6725:6732 c5 <> double_S thm
prf 6793:6803 <> nth_error_x
binder 6812:6812 <> X:91
R6823:6825 Coq.Init.Datatypes <> nat ind
binder 6820:6820 <> n:92
R6831:6834 Coq.Init.Datatypes <> list ind
R6836:6836 c5 <> X:91 var
binder 6828:6828 <> l:93
R6842:6842 c5 <> X:91 var
binder 6839:6839 <> x:94
R6870:6872 Coq.Init.Logic <> ::type_scope:x_'='_x not
R6848:6856 Coq.Lists.List <> nth_error def
R6866:6866 Coq.Init.Datatypes <> S constr
R6868:6868 c5 <> n:92 var
R6860:6861 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6859:6859 c5 <> x:94 var
R6862:6862 c5 <> l:93 var
R6873:6881 Coq.Lists.List <> nth_error def
R6885:6885 c5 <> n:92 var
R6883:6883 c5 <> l:93 var
prf 6947:6966 <> nth_error_after_last
binder 6977:6977 <> X:95
R6991:6993 Coq.Init.Datatypes <> nat ind
binder 6987:6987 <> n:96
R7002:7005 Coq.Init.Datatypes <> list ind
R7007:7007 c5 <> X:95 var
binder 6998:6998 <> l:97
R7025:7030 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R7021:7023 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7013:7018 Coq.Init.Datatypes <> length def
R7020:7020 c5 <> l:97 var
R7024:7024 c5 <> n:96 var
R7044:7046 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7031:7039 Coq.Lists.List <> nth_error def
R7043:7043 c5 <> n:96 var
R7041:7041 c5 <> l:97 var
R7047:7050 Coq.Init.Datatypes <> None constr
R7265:7275 c5 <> nth_error_x thm
R7265:7275 c5 <> nth_error_x thm
R7265:7275 c5 <> nth_error_x thm
def 7351:7356 <> square
binder 7358:7358 <> n:98
R7364:7366 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7363:7363 c5 <> n:98 var
R7367:7367 c5 <> n:98 var
prf 7379:7388 <> mult_assoc
R7407:7409 Coq.Init.Datatypes <> nat ind
binder 7399:7399 <> n:99
binder 7401:7401 <> m:100
binder 7403:7403 <> p:101
R7425:7427 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7415:7418 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7424:7424 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7414:7414 c5 <> n:99 var
R7420:7422 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7419:7419 c5 <> m:100 var
R7423:7423 c5 <> p:101 var
R7428:7428 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7434:7437 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7430:7432 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7429:7429 c5 <> n:99 var
R7433:7433 c5 <> m:100 var
R7438:7438 c5 <> p:101 var
prf 7467:7475 <> mult_comm
R7489:7491 Coq.Init.Datatypes <> nat ind
binder 7484:7484 <> n:102
binder 7486:7486 <> m:103
R7499:7501 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7496:7497 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7495:7495 c5 <> n:102 var
R7498:7498 c5 <> m:103 var
R7503:7503 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7502:7502 c5 <> m:103 var
R7504:7504 c5 <> n:102 var
prf 7531:7541 <> square_mult
binder 7552:7552 <> n:104
binder 7554:7554 <> m:105
R7571:7573 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7557:7562 c5 <> square def
R7566:7568 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7565:7565 c5 <> n:104 var
R7569:7569 c5 <> m:105 var
R7582:7584 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7574:7579 c5 <> square def
R7581:7581 c5 <> n:104 var
R7585:7590 c5 <> square def
R7592:7592 c5 <> m:105 var
R7621:7626 c5 <> square def
R7642:7651 c5 <> mult_assoc prfax
R7642:7651 c5 <> mult_assoc prfax
R7642:7651 c5 <> mult_assoc prfax
R7677:7679 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7673:7675 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7669:7671 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7685:7687 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7681:7683 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7677:7679 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7673:7675 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7669:7671 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7685:7687 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7681:7683 Coq.Init.Nat <> ::nat_scope:x_'*'_x not
R7707:7715 c5 <> mult_comm prfax
R7707:7715 c5 <> mult_comm prfax
R7707:7715 c5 <> mult_comm prfax
R7724:7733 c5 <> mult_assoc prfax
R7724:7733 c5 <> mult_assoc prfax
R7765:7774 c5 <> mult_assoc prfax
R7765:7774 c5 <> mult_assoc prfax
R7765:7774 c5 <> mult_assoc prfax
def 7811:7813 <> foo
R7819:7821 Coq.Init.Datatypes <> nat ind
binder 7816:7816 <> x:106
prf 7836:7847 <> silly_fact_1
binder 7858:7858 <> m:107
R7870:7872 Coq.Init.Logic <> ::type_scope:x_'='_x not
R7866:7868 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R7861:7863 c5 <> foo def
R7865:7865 c5 <> m:107 var
R7884:7886 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R7873:7875 c5 <> foo def
R7879:7881 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R7878:7878 c5 <> m:107 var
def 7941:7943 <> bar
binder 7945:7945 <> x:108
R7958:7958 c5 <> x:108 var
R7969:7969 Coq.Init.Datatypes <> O constr
R7980:7980 Coq.Init.Datatypes <> S constr
prf 8002:8020 <> silly_fact_2_FAILED
binder 8031:8031 <> m:110
R8043:8045 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8039:8041 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8034:8036 c5 <> bar def
R8038:8038 c5 <> m:110 var
R8057:8059 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8046:8048 c5 <> bar def
R8052:8054 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8051:8051 c5 <> m:110 var
def 8196:8203 <> sillyfun
R8210:8212 Coq.Init.Datatypes <> nat ind
binder 8206:8206 <> n:111
R8217:8220 Coq.Init.Datatypes <> bool ind
R8231:8234 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R8230:8230 c5 <> n:111 var
R8259:8262 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R8258:8258 c5 <> n:111 var
R8283:8287 Coq.Init.Datatypes <> false constr
R8270:8274 Coq.Init.Datatypes <> false constr
R8242:8246 Coq.Init.Datatypes <> false constr
prf 8299:8312 <> sillyfun_false
R8328:8330 Coq.Init.Datatypes <> nat ind
binder 8324:8324 <> n:112
R8346:8348 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8336:8343 c5 <> sillyfun def
R8345:8345 c5 <> n:112 var
R8349:8353 Coq.Init.Datatypes <> false constr
R8382:8389 c5 <> sillyfun def
R8406:8409 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R8406:8409 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R8446:8449 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
R8446:8449 Coq.Init.Nat <> ::nat_scope:x_'=?'_x not
def 8507:8511 <> split
binder 8514:8514 <> X:113
binder 8516:8516 <> Y:114
R8531:8534 Coq.Init.Datatypes <> list ind
R8538:8538 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R8537:8537 c5 <> X:113 var
R8539:8539 c5 <> Y:114 var
binder 8527:8527 <> l:115
R8560:8560 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R8567:8571 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R8578:8578 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R8561:8564 Coq.Init.Datatypes <> list ind
R8566:8566 c5 <> X:113 var
R8572:8575 Coq.Init.Datatypes <> list ind
R8577:8577 c5 <> Y:114 var
R8591:8591 c5 <> l:115 var
R8602:8603 c5 <> ::list_scope:'['_']' not
R8608:8608 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8611:8612 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8615:8615 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8609:8610 c5 <> ::list_scope:'['_']' not
R8613:8614 c5 <> ::list_scope:'['_']' not
R8627:8630 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R8621:8621 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8623:8624 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8626:8626 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8631:8631 Coq.Init.Nat <> t def
R8648:8652 c5 <> split:116 def
R8669:8669 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8672:8673 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8676:8676 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8681:8681 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8689:8690 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8698:8698 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8683:8686 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R8692:8695 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
prf 8726:8729 <> nail
binder 8740:8740 <> X:118
R8751:8751 c5 <> X:118 var
binder 8749:8749 <> x:119
R8761:8764 Coq.Init.Datatypes <> list ind
R8766:8766 c5 <> X:118 var
binder 8754:8755 <> l1:120
binder 8757:8758 <> l2:121
R8779:8782 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8774:8776 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8772:8773 c5 <> l1:120 var
R8777:8778 c5 <> l2:121 var
R8788:8790 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8784:8785 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R8783:8783 c5 <> x:119 var
R8786:8787 c5 <> l1:120 var
R8792:8793 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R8791:8791 c5 <> x:119 var
R8794:8795 c5 <> l2:121 var
prf 8894:8906 <> combine_split
binder 8917:8917 <> X:122
binder 8919:8919 <> Y:123
R8926:8929 Coq.Init.Datatypes <> list ind
R8933:8935 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R8932:8932 c5 <> X:122 var
R8936:8936 c5 <> Y:123 var
binder 8922:8922 <> l:124
binder 8940:8941 <> l1:125
binder 8943:8944 <> l2:126
R8967:8972 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R8956:8958 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8949:8953 c5 <> split def
R8955:8955 c5 <> l:124 var
R8959:8959 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8962:8963 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8966:8966 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R8960:8961 c5 <> l1:125 var
R8964:8965 c5 <> l2:126 var
R8986:8988 Coq.Init.Logic <> ::type_scope:x_'='_x not
R8973:8979 Coq.Lists.List <> combine def
R8984:8985 c5 <> l2:126 var
R8981:8982 c5 <> l1:125 var
R8989:8989 c5 <> l:124 var
R9293:9297 c5 <> split def
R9293:9297 c5 <> split def
R9387:9390 c5 <> nail thm
R9387:9390 c5 <> nail thm
prf 9816:9829 <> combine_split'
binder 9840:9840 <> X:127
binder 9842:9842 <> Y:128
R9849:9852 Coq.Init.Datatypes <> list ind
R9856:9858 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
R9855:9855 c5 <> X:127 var
R9859:9859 c5 <> Y:128 var
binder 9845:9845 <> l:129
binder 9863:9864 <> l1:130
binder 9866:9867 <> l2:131
R9890:9895 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9879:9881 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9872:9876 c5 <> split def
R9878:9878 c5 <> l:129 var
R9882:9882 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R9885:9886 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R9889:9889 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
R9883:9884 c5 <> l1:130 var
R9887:9888 c5 <> l2:131 var
R9909:9911 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9896:9902 Coq.Lists.List <> combine def
R9907:9908 c5 <> l2:131 var
R9904:9905 c5 <> l1:130 var
R9912:9912 c5 <> l:129 var
R10072:10076 c5 <> split def
R10072:10076 c5 <> split def
R10138:10141 c5 <> nail thm
R10138:10141 c5 <> nail thm
def 10192:10200 <> sillyfun1
R10207:10209 Coq.Init.Datatypes <> nat ind
binder 10203:10203 <> n:132
R10214:10217 Coq.Init.Datatypes <> bool ind
R10227:10229 Coq.Init.Nat <> eqb def
R10231:10231 c5 <> n:132 var
R10255:10257 Coq.Init.Nat <> eqb def
R10259:10259 c5 <> n:132 var
R10280:10284 Coq.Init.Datatypes <> false constr
R10268:10271 Coq.Init.Datatypes <> true constr
R10240:10243 Coq.Init.Datatypes <> true constr
prf 10296:10308 <> sillyfun1_odd
R10324:10326 Coq.Init.Datatypes <> nat ind
binder 10320:10320 <> n:133
R10353:10361 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10346:10348 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10335:10343 c5 <> sillyfun1 def
R10345:10345 c5 <> n:133 var
R10349:10352 Coq.Init.Datatypes <> true constr
R10367:10369 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10362:10364 Coq.Init.Nat <> odd def
R10366:10366 c5 <> n:133 var
R10370:10373 Coq.Init.Datatypes <> true constr
R10402:10410 c5 <> sillyfun1 def
R10430:10432 Coq.Init.Nat <> eqb def
R10430:10432 Coq.Init.Nat <> eqb def
R10459:10466 c5 <> eqb_true thm
R10459:10466 c5 <> eqb_true thm
R10529:10531 Coq.Init.Nat <> eqb def
R10529:10531 Coq.Init.Nat <> eqb def
R10560:10567 c5 <> eqb_true thm
R10560:10567 c5 <> eqb_true thm
prf 10725:10738 <> sillyfun1_odd'
R10754:10756 Coq.Init.Datatypes <> nat ind
binder 10750:10750 <> n:134
R10783:10791 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10776:10778 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10765:10773 c5 <> sillyfun1 def
R10775:10775 c5 <> n:134 var
R10779:10782 Coq.Init.Datatypes <> true constr
R10797:10799 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10792:10794 Coq.Init.Nat <> odd def
R10796:10796 c5 <> n:134 var
R10800:10803 Coq.Init.Datatypes <> true constr
R10832:10840 c5 <> sillyfun1 def
R10860:10862 Coq.Init.Nat <> eqb def
R10860:10862 Coq.Init.Nat <> eqb def
prf 10890:10911 <> bool_fn_applied_thrice
R10933:10936 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10929:10932 Coq.Init.Datatypes <> bool ind