forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
General.glob
924 lines (924 loc) · 39.6 KB
/
General.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
DIGEST d420f22797680f5c1625fd40de46c198
FGeneral
R2136:2140 Coq.omega.Omega <> <> lib
R2158:2166 Coq.setoid_ring.ArithRing <> <> lib
R2303:2306 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R2303:2306 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R2374:2378 Coq.Init.Logic <> False ind
R2363:2367 Coq.Init.Logic <> False ind
R2374:2378 Coq.Init.Logic <> False ind
R2363:2367 Coq.Init.Logic <> False ind
R2453:2456 Coq.Init.Logic <> True ind
R2443:2446 Coq.Init.Logic <> True ind
R2453:2456 Coq.Init.Logic <> True ind
R2443:2446 Coq.Init.Logic <> True ind
R2485:2487 Coq.Init.Logic <> :type_scope:x_'='_x not
R2480:2484 Coq.Init.Datatypes <> false constr
R2488:2491 Coq.Init.Datatypes <> true constr
R2485:2487 Coq.Init.Logic <> :type_scope:x_'='_x not
R2480:2484 Coq.Init.Datatypes <> false constr
R2488:2491 Coq.Init.Datatypes <> true constr
R2517:2523 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R2525:2526 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R2517:2523 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R2525:2526 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R2677:2681 Coq.Init.Logic <> False ind
R3533:3535 Coq.Init.Logic <> :type_scope:x_'='_x not
R3533:3535 Coq.Init.Logic <> :type_scope:x_'='_x not
R3672:3675 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R3668:3668 Coq.Init.Datatypes <> S constr
R3676:3676 Coq.Init.Datatypes <> S constr
R3672:3675 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R3668:3668 Coq.Init.Datatypes <> S constr
R3676:3676 Coq.Init.Datatypes <> S constr
R3727:3729 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3723:3723 Coq.Init.Datatypes <> S constr
R3730:3730 Coq.Init.Datatypes <> S constr
R3727:3729 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3723:3723 Coq.Init.Datatypes <> S constr
R3730:3730 Coq.Init.Datatypes <> S constr
R3779:3782 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3775:3775 Coq.Init.Datatypes <> S constr
R3783:3783 Coq.Init.Datatypes <> S constr
R3779:3782 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3775:3775 Coq.Init.Datatypes <> S constr
R3783:3783 Coq.Init.Datatypes <> S constr
R3834:3836 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3830:3830 Coq.Init.Datatypes <> S constr
R3837:3837 Coq.Init.Datatypes <> S constr
R3834:3836 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3830:3830 Coq.Init.Datatypes <> S constr
R3837:3837 Coq.Init.Datatypes <> S constr
R3849:3850 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3795:3797 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R3742:3743 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3688:3690 Coq.Init.Peano <> :nat_scope:x_'<='_x not
prf 3891:3908 <> times_distributive
R3935:3937 Coq.Init.Logic <> :type_scope:x_'='_x not
R3926:3926 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3930:3933 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3928:3928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3927:3927 General <> m var
R3929:3929 General <> n var
R3934:3934 General <> p var
R3941:3943 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3939:3939 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3938:3938 General <> m var
R3940:3940 General <> p var
R3945:3947 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3944:3944 General <> n var
R3948:3948 General <> p var
prf 3989:4007 <> times_distributive2
R4041:4043 Coq.Init.Logic <> :type_scope:x_'='_x not
R4028:4028 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4032:4036 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4040:4040 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4030:4030 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4029:4029 General <> m var
R4031:4031 General <> n var
R4038:4038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4037:4037 General <> p var
R4039:4039 General <> q var
R4061:4063 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4055:4057 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4047:4049 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4045:4045 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4044:4044 General <> m var
R4046:4046 General <> p var
R4051:4053 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4050:4050 General <> n var
R4054:4054 General <> p var
R4059:4059 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4058:4058 General <> m var
R4060:4060 General <> q var
R4065:4065 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4064:4064 General <> n var
R4066:4066 General <> q var
prf 4107:4120 <> times_positive
R4138:4141 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4145:4148 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4152:4153 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4150:4150 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4149:4149 General <> m var
R4151:4151 General <> n var
R4143:4143 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4142:4142 General <> n var
R4136:4136 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4135:4135 General <> m var
R4238:4240 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4243:4245 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4246:4246 Coq.Init.Datatypes <> S constr
R4238:4240 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4243:4245 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4246:4246 Coq.Init.Datatypes <> S constr
prf 4288:4302 <> times_monotonic
R4331:4334 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4341:4344 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4352:4355 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4363:4366 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4374:4376 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4369:4371 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4367:4368 General <> m1 var
R4372:4373 General <> m2 var
R4379:4381 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4377:4378 General <> n1 var
R4382:4383 General <> n2 var
R4358:4360 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4356:4357 General <> m2 var
R4361:4362 General <> n2 var
R4347:4349 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4345:4346 General <> m1 var
R4350:4351 General <> n1 var
R4336:4338 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4339:4340 General <> m2 var
R4327:4328 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4329:4330 General <> m1 var
R4432:4434 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4427:4429 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4432:4434 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4427:4429 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4474:4476 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4469:4471 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4474:4476 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4469:4471 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4500:4518 General <> times_distributive2 thm
R4500:4518 General <> times_distributive2 thm
R4500:4518 General <> times_distributive2 thm
R4527:4529 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4568:4570 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4551:4553 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4530:4530 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4538:4542 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4550:4550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4533:4535 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4545:4547 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4556:4559 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4567:4567 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4562:4564 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4571:4571 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4579:4582 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4574:4576 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4527:4529 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4568:4570 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4551:4553 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4530:4530 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4538:4542 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4550:4550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4533:4535 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4545:4547 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4556:4559 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4567:4567 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4562:4564 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4571:4571 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4579:4582 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4574:4576 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4626:4628 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4636:4636 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4629:4632 Coq.Init.Peano <> pred syndef
R4626:4628 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4636:4636 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4629:4632 Coq.Init.Peano <> pred syndef
R4661:4663 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4675:4677 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4692:4692 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4678:4681 Coq.Init.Peano <> pred syndef
R4686:4688 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4661:4663 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4675:4677 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4692:4692 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4678:4681 Coq.Init.Peano <> pred syndef
R4686:4688 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4714:4732 General <> times_distributive2 thm
R4714:4732 General <> times_distributive2 thm
R4714:4732 General <> times_distributive2 thm
R4784:4786 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4761:4764 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4783:4783 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4757:4759 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4750:4753 Coq.Init.Peano <> pred syndef
R4779:4781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4765:4768 Coq.Init.Peano <> pred syndef
R4773:4775 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4794:4796 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4787:4790 Coq.Init.Peano <> pred syndef
R4797:4800 Coq.Init.Peano <> pred syndef
R4805:4807 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4821:4821 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4838:4841 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4824:4826 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4827:4827 Coq.Init.Datatypes <> S constr
R4830:4833 Coq.Init.Peano <> pred syndef
R4842:4842 Coq.Init.Datatypes <> S constr
R4845:4848 Coq.Init.Peano <> pred syndef
R4853:4855 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4869:4869 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4886:4889 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4872:4874 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4875:4875 Coq.Init.Datatypes <> S constr
R4878:4881 Coq.Init.Peano <> pred syndef
R4784:4786 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4761:4764 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4783:4783 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4757:4759 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4750:4753 Coq.Init.Peano <> pred syndef
R4779:4781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4765:4768 Coq.Init.Peano <> pred syndef
R4773:4775 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4794:4796 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4787:4790 Coq.Init.Peano <> pred syndef
R4797:4800 Coq.Init.Peano <> pred syndef
R4805:4807 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4821:4821 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4838:4841 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4824:4826 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4827:4827 Coq.Init.Datatypes <> S constr
R4830:4833 Coq.Init.Peano <> pred syndef
R4842:4842 Coq.Init.Datatypes <> S constr
R4845:4848 Coq.Init.Peano <> pred syndef
R4853:4855 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4821:4821 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4838:4841 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4824:4826 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4827:4827 Coq.Init.Datatypes <> S constr
R4830:4833 Coq.Init.Peano <> pred syndef
R4842:4842 Coq.Init.Datatypes <> S constr
R4845:4848 Coq.Init.Peano <> pred syndef
R4853:4855 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4869:4869 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4886:4889 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4872:4874 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4875:4875 Coq.Init.Datatypes <> S constr
R4878:4881 Coq.Init.Peano <> pred syndef
R4869:4869 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4886:4889 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4872:4874 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4875:4875 Coq.Init.Datatypes <> S constr
R4878:4881 Coq.Init.Peano <> pred syndef
R4869:4869 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4886:4889 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4872:4874 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4875:4875 Coq.Init.Datatypes <> S constr
R4878:4881 Coq.Init.Peano <> pred syndef
R4869:4869 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4886:4889 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4872:4874 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R4875:4875 Coq.Init.Datatypes <> S constr
R4878:4881 Coq.Init.Peano <> pred syndef
prf 4928:4943 <> times_monotonic2
R4972:4975 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4982:4985 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4994:4997 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5005:5008 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5016:5018 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5011:5013 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5009:5010 General <> m1 var
R5014:5015 General <> m2 var
R5021:5023 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5019:5020 General <> n1 var
R5024:5025 General <> n2 var
R5000:5002 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4998:4999 General <> m2 var
R5003:5004 General <> n2 var
R4988:4991 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4986:4987 General <> m1 var
R4992:4993 General <> n1 var
R4977:4979 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4980:4981 General <> m2 var
R4968:4969 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4970:4971 General <> m1 var
R5074:5076 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5069:5071 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5074:5076 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5069:5071 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5116:5118 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5111:5113 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5116:5118 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5111:5113 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5142:5160 General <> times_distributive2 thm
R5142:5160 General <> times_distributive2 thm
R5142:5160 General <> times_distributive2 thm
R5172:5174 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5213:5215 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5196:5198 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5175:5175 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5183:5187 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5195:5195 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5178:5180 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5190:5192 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5201:5204 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5212:5212 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5207:5209 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5216:5216 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5224:5227 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5219:5221 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5172:5174 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5213:5215 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5196:5198 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5175:5175 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5183:5187 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5195:5195 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5178:5180 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5190:5192 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5201:5204 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5212:5212 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5207:5209 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5216:5216 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5224:5227 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5219:5221 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5252:5254 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5262:5262 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5255:5258 Coq.Init.Peano <> pred syndef
R5252:5254 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5262:5262 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5255:5258 Coq.Init.Peano <> pred syndef
R5287:5289 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5301:5303 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5318:5318 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5304:5307 Coq.Init.Peano <> pred syndef
R5312:5314 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5287:5289 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5301:5303 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5318:5318 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5304:5307 Coq.Init.Peano <> pred syndef
R5312:5314 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5340:5358 General <> times_distributive2 thm
R5340:5358 General <> times_distributive2 thm
R5340:5358 General <> times_distributive2 thm
R5410:5412 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5387:5390 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5409:5409 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5383:5385 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5376:5379 Coq.Init.Peano <> pred syndef
R5405:5407 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5391:5394 Coq.Init.Peano <> pred syndef
R5399:5401 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5420:5422 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5413:5416 Coq.Init.Peano <> pred syndef
R5423:5426 Coq.Init.Peano <> pred syndef
R5431:5433 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5447:5447 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5464:5467 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5450:5452 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5453:5453 Coq.Init.Datatypes <> S constr
R5456:5459 Coq.Init.Peano <> pred syndef
R5468:5468 Coq.Init.Datatypes <> S constr
R5471:5474 Coq.Init.Peano <> pred syndef
R5479:5481 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5495:5495 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5512:5515 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5498:5500 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5501:5501 Coq.Init.Datatypes <> S constr
R5504:5507 Coq.Init.Peano <> pred syndef
R5410:5412 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5387:5390 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5409:5409 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5383:5385 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5376:5379 Coq.Init.Peano <> pred syndef
R5405:5407 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5391:5394 Coq.Init.Peano <> pred syndef
R5399:5401 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5420:5422 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5413:5416 Coq.Init.Peano <> pred syndef
R5423:5426 Coq.Init.Peano <> pred syndef
R5431:5433 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5447:5447 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5464:5467 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5450:5452 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5453:5453 Coq.Init.Datatypes <> S constr
R5456:5459 Coq.Init.Peano <> pred syndef
R5468:5468 Coq.Init.Datatypes <> S constr
R5471:5474 Coq.Init.Peano <> pred syndef
R5479:5481 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5447:5447 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5464:5467 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5450:5452 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5453:5453 Coq.Init.Datatypes <> S constr
R5456:5459 Coq.Init.Peano <> pred syndef
R5468:5468 Coq.Init.Datatypes <> S constr
R5471:5474 Coq.Init.Peano <> pred syndef
R5479:5481 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5495:5495 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5512:5515 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5498:5500 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5501:5501 Coq.Init.Datatypes <> S constr
R5504:5507 Coq.Init.Peano <> pred syndef
R5495:5495 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5512:5515 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5498:5500 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5501:5501 Coq.Init.Datatypes <> S constr
R5504:5507 Coq.Init.Peano <> pred syndef
R5495:5495 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5512:5515 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5498:5500 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5501:5501 Coq.Init.Datatypes <> S constr
R5504:5507 Coq.Init.Peano <> pred syndef
R5495:5495 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5512:5515 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5498:5500 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5501:5501 Coq.Init.Datatypes <> S constr
R5504:5507 Coq.Init.Peano <> pred syndef
R5591:5593 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5574:5576 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5553:5553 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5561:5565 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5573:5573 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5556:5558 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5568:5570 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5579:5582 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5590:5590 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5585:5587 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5594:5594 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5602:5605 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5597:5599 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5591:5593 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5574:5576 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5553:5553 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5561:5565 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5573:5573 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5556:5558 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5568:5570 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5579:5582 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5590:5590 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5585:5587 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R5594:5594 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5602:5605 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5597:5599 Coq.Init.Peano <> :nat_scope:x_'-'_x not
def 5659:5661 <> exp
R5668:5670 Coq.Init.Datatypes <> nat ind
R5668:5670 Coq.Init.Datatypes <> nat ind
R5685:5687 Coq.Init.Datatypes <> nat ind
R5698:5698 General <> n var
R5707:5707 Coq.Init.Datatypes <> O constr
R5716:5716 Coq.Init.Datatypes <> S constr
R5724:5726 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5723:5723 General <> m var
R5727:5729 General <> exp def
R5733:5733 General <> n var
R5731:5731 General <> m var
R5762:5764 General <> exp def
not 5750:5750 <> ::x_'^'_x
prf 5779:5790 <> exp_positive
R5808:5811 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5819:5820 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5812:5814 General <> exp def
R5818:5818 General <> n var
R5816:5816 General <> m var
R5806:5806 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5805:5805 General <> m var
R5868:5869 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5866:5866 Coq.Arith.PeanoNat <> :nat_scope:x_'^'_x not
R5868:5869 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5866:5866 Coq.Arith.PeanoNat <> :nat_scope:x_'^'_x not
R5897:5910 General <> times_positive thm
prf 5929:5938 <> max_is_max
R5966:5969 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5961:5964 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5954:5956 Coq.Init.Peano <> max syndef
R5960:5960 General <> n var
R5958:5958 General <> m var
R5965:5965 General <> m var
R5977:5980 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5970:5972 Coq.Init.Peano <> max syndef
R5976:5976 General <> n var
R5974:5974 General <> m var
R5981:5981 General <> n var
prf 6115:6122 <> max_succ
R6148:6150 Coq.Init.Logic <> :type_scope:x_'='_x not
R6137:6137 Coq.Init.Datatypes <> S constr
R6140:6142 Coq.Init.Peano <> max syndef
R6146:6146 General <> n var
R6144:6144 General <> m var
R6151:6153 Coq.Init.Peano <> max syndef
R6162:6162 Coq.Init.Datatypes <> S constr
R6164:6164 General <> n var
R6156:6156 Coq.Init.Datatypes <> S constr
R6158:6158 General <> m var
prf 6223:6230 <> max_pred
R6259:6261 Coq.Init.Logic <> :type_scope:x_'='_x not
R6245:6248 Coq.Init.Peano <> pred syndef
R6251:6253 Coq.Init.Peano <> max syndef
R6257:6257 General <> n var
R6255:6255 General <> m var
R6262:6264 Coq.Init.Peano <> max syndef
R6276:6279 Coq.Init.Peano <> pred syndef
R6281:6281 General <> n var
R6267:6270 Coq.Init.Peano <> pred syndef
R6272:6272 General <> m var
prf 6358:6364 <> max_max
R6394:6397 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6403:6406 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6399:6401 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6398:6398 General <> m var
R6402:6402 General <> n var
R6408:6410 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6407:6407 General <> m var
R6411:6411 General <> p var
R6383:6386 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6382:6382 General <> m var
R6387:6389 Coq.Init.Peano <> max syndef
R6393:6393 General <> p var
R6391:6391 General <> n var
R6521:6524 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6525:6528 Coq.Init.Peano <> pred syndef
R6531:6533 Coq.Init.Peano <> max syndef
R6521:6524 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6525:6528 Coq.Init.Peano <> pred syndef
R6531:6533 Coq.Init.Peano <> max syndef
R6560:6567 General <> max_pred thm
R6560:6567 General <> max_pred thm
R6560:6567 General <> max_pred thm
R6597:6600 Coq.Init.Peano <> pred syndef
R6588:6591 Coq.Init.Peano <> pred syndef
R6597:6600 Coq.Init.Peano <> pred syndef
R6588:6591 Coq.Init.Peano <> pred syndef
prf 6639:6646 <> max_max2
R6669:6672 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6678:6681 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6683:6685 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6682:6682 General <> k var
R6686:6688 Coq.Init.Peano <> max syndef
R6692:6692 General <> n var
R6690:6690 General <> m var
R6674:6676 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6673:6673 General <> k var
R6677:6677 General <> n var
R6665:6667 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6664:6664 General <> k var
R6668:6668 General <> m var
R6751:6754 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6745:6748 Coq.Init.Peano <> pred syndef
R6755:6757 Coq.Init.Peano <> max syndef
R6751:6754 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6745:6748 Coq.Init.Peano <> pred syndef
R6755:6757 Coq.Init.Peano <> max syndef
prf 6815:6822 <> max_zero
R6843:6845 Coq.Init.Logic <> :type_scope:x_'='_x not
R6836:6838 Coq.Init.Peano <> max syndef
R6840:6840 General <> m var
R6846:6846 General <> m var
prf 6893:6900 <> max_plus
R6927:6929 Coq.Init.Logic <> :type_scope:x_'='_x not
R6924:6925 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6917:6919 Coq.Init.Peano <> max syndef
R6923:6923 General <> n var
R6921:6921 General <> m var
R6926:6926 General <> k var
R6930:6932 Coq.Init.Peano <> max syndef
R6942:6942 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6941:6941 General <> n var
R6943:6943 General <> k var
R6936:6936 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6935:6935 General <> m var
R6937:6937 General <> k var
R7038:7041 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7022:7024 Coq.Init.Peano <> max syndef
R7029:7029 Coq.Init.Datatypes <> S constr
R7034:7034 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7042:7042 Coq.Init.Datatypes <> S constr
R7046:7046 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7038:7041 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7022:7024 Coq.Init.Peano <> max syndef
R7029:7029 Coq.Init.Datatypes <> S constr
R7034:7034 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7042:7042 Coq.Init.Datatypes <> S constr
R7046:7046 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7062:7071 General <> max_is_max thm
R7090:7093 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7083:7083 Coq.Init.Datatypes <> S constr
R7087:7087 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7094:7096 Coq.Init.Peano <> max syndef
R7101:7101 Coq.Init.Datatypes <> S constr
R7105:7105 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7090:7093 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7083:7083 Coq.Init.Datatypes <> S constr
R7087:7087 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7094:7096 Coq.Init.Peano <> max syndef
R7101:7101 Coq.Init.Datatypes <> S constr
R7105:7105 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7121:7128 General <> max_max2 thm
R7190:7193 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7175:7177 Coq.Init.Peano <> max syndef
R7181:7181 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7182:7182 Coq.Init.Datatypes <> S constr
R7195:7196 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7197:7197 Coq.Init.Datatypes <> S constr
R7190:7193 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7175:7177 Coq.Init.Peano <> max syndef
R7181:7181 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7182:7182 Coq.Init.Datatypes <> S constr
R7195:7196 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7197:7197 Coq.Init.Datatypes <> S constr
R7215:7224 General <> max_is_max thm
R7243:7246 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7237:7238 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7239:7239 Coq.Init.Datatypes <> S constr
R7247:7249 Coq.Init.Peano <> max syndef
R7253:7253 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7254:7254 Coq.Init.Datatypes <> S constr
R7243:7246 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7237:7238 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7239:7239 Coq.Init.Datatypes <> S constr
R7247:7249 Coq.Init.Peano <> max syndef
R7253:7253 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7254:7254 Coq.Init.Datatypes <> S constr
R7274:7281 General <> max_max2 thm
prf 7314:7322 <> max_minus
R7349:7351 Coq.Init.Logic <> :type_scope:x_'='_x not
R7346:7347 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R7339:7341 Coq.Init.Peano <> max syndef
R7345:7345 General <> n var
R7343:7343 General <> m var
R7348:7348 General <> k var
R7352:7354 Coq.Init.Peano <> max syndef
R7364:7364 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R7363:7363 General <> n var
R7365:7365 General <> k var
R7358:7358 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R7357:7357 General <> m var
R7359:7359 General <> k var
R7438:7445 General <> max_zero thm
R7438:7445 General <> max_zero thm
R7438:7445 General <> max_zero thm
prf 7488:7500 <> max_monotonic
R7532:7535 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7544:7547 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7557:7560 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7548:7550 Coq.Init.Peano <> max syndef
R7555:7556 General <> m2 var
R7552:7553 General <> m1 var
R7561:7563 Coq.Init.Peano <> max syndef
R7568:7569 General <> n2 var
R7565:7566 General <> n1 var
R7538:7541 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7536:7537 General <> m2 var
R7542:7543 General <> n2 var
R7526:7529 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7524:7525 General <> m1 var
R7530:7531 General <> n1 var
R7627:7629 Coq.Init.Logic <> :type_scope:x_'='_x not
R7627:7629 Coq.Init.Logic <> :type_scope:x_'='_x not
R7661:7663 Coq.Init.Logic <> :type_scope:x_'='_x not
R7661:7663 Coq.Init.Logic <> :type_scope:x_'='_x not
R7707:7709 Coq.Init.Logic <> :type_scope:x_'='_x not
R7707:7709 Coq.Init.Logic <> :type_scope:x_'='_x not
R7752:7754 Coq.Init.Logic <> :type_scope:x_'='_x not
R7752:7754 Coq.Init.Logic <> :type_scope:x_'='_x not
R7791:7793 Coq.Init.Logic <> :type_scope:x_'='_x not
R7783:7785 Coq.Init.Peano <> max syndef
R7791:7793 Coq.Init.Logic <> :type_scope:x_'='_x not
R7783:7785 Coq.Init.Peano <> max syndef
R7850:7853 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7854:7857 Coq.Init.Peano <> pred syndef
R7850:7853 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7854:7857 Coq.Init.Peano <> pred syndef
R7885:7888 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7877:7879 Coq.Init.Peano <> max syndef
R7889:7892 Coq.Init.Peano <> pred syndef
R7895:7897 Coq.Init.Peano <> max syndef
R7885:7888 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7877:7879 Coq.Init.Peano <> max syndef
R7889:7892 Coq.Init.Peano <> pred syndef
R7895:7897 Coq.Init.Peano <> max syndef
R7935:7942 General <> max_pred thm
R7935:7942 General <> max_pred thm
R7935:7942 General <> max_pred thm
prf 7980:7992 <> max_succ_zero
R8023:8026 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8027:8031 Coq.Init.Logic <> False ind
R8019:8021 Coq.Init.Logic <> :type_scope:x_'='_x not
R8008:8010 Coq.Init.Peano <> max syndef
R8015:8015 Coq.Init.Datatypes <> S constr
R8017:8017 General <> n var
R8012:8012 General <> k var
R8071:8074 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8060:8062 Coq.Init.Peano <> max syndef
R8067:8067 Coq.Init.Datatypes <> S constr
R8075:8075 Coq.Init.Datatypes <> S constr
R8071:8074 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8060:8062 Coq.Init.Peano <> max syndef
R8067:8067 Coq.Init.Datatypes <> S constr
R8075:8075 Coq.Init.Datatypes <> S constr
R8091:8100 General <> max_is_max thm
R8167:8169 Coq.Init.Logic <> :type_scope:x_'='_x not
R8156:8158 Coq.Init.Peano <> max syndef
R8163:8163 Coq.Init.Datatypes <> S constr
R8167:8169 Coq.Init.Logic <> :type_scope:x_'='_x not
R8156:8158 Coq.Init.Peano <> max syndef
R8163:8163 Coq.Init.Datatypes <> S constr
R8243:8245 Coq.Init.Logic <> :type_scope:x_'='_x not
R8234:8236 Coq.Init.Peano <> max syndef
R8243:8245 Coq.Init.Logic <> :type_scope:x_'='_x not
R8234:8236 Coq.Init.Peano <> max syndef
R8446:8449 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8437:8439 Coq.Init.Peano <> max syndef
R8446:8449 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8437:8439 Coq.Init.Peano <> max syndef
R8470:8472 Coq.Init.Logic <> :type_scope:x_'='_x not
R8495:8498 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8488:8490 Coq.Init.Peano <> max syndef
R8542:8544 Coq.Init.Logic <> :type_scope:x_'='_x not
R8567:8570 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8560:8562 Coq.Init.Peano <> max syndef
R8266:8268 Coq.Init.Logic <> :type_scope:x_'='_x not
R8291:8294 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8284:8286 Coq.Init.Peano <> max syndef
R8338:8340 Coq.Init.Logic <> :type_scope:x_'='_x not
R8363:8366 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R8356:8358 Coq.Init.Peano <> max syndef
R8188:8192 Coq.Init.Logic <> False ind
prf 8650:8659 <> min_is_min
R8687:8690 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8682:8685 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8675:8677 Coq.Init.Peano <> min syndef
R8681:8681 General <> n var
R8679:8679 General <> m var
R8686:8686 General <> m var
R8698:8701 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8691:8693 Coq.Init.Peano <> min syndef
R8697:8697 General <> n var
R8695:8695 General <> m var
R8702:8702 General <> n var
prf 8836:8843 <> min_succ
R8869:8871 Coq.Init.Logic <> :type_scope:x_'='_x not
R8858:8858 Coq.Init.Datatypes <> S constr
R8861:8863 Coq.Init.Peano <> min syndef
R8867:8867 General <> n var
R8865:8865 General <> m var
R8872:8874 Coq.Init.Peano <> min syndef
R8883:8883 Coq.Init.Datatypes <> S constr
R8885:8885 General <> n var
R8877:8877 Coq.Init.Datatypes <> S constr
R8879:8879 General <> m var
prf 8944:8951 <> min_pred
R8980:8982 Coq.Init.Logic <> :type_scope:x_'='_x not
R8966:8969 Coq.Init.Peano <> pred syndef
R8972:8974 Coq.Init.Peano <> min syndef
R8978:8978 General <> n var
R8976:8976 General <> m var
R8983:8985 Coq.Init.Peano <> min syndef
R8997:9000 Coq.Init.Peano <> pred syndef
R9002:9002 General <> n var
R8988:8991 Coq.Init.Peano <> pred syndef
R8993:8993 General <> m var
prf 9079:9086 <> min_zero
R9107:9109 Coq.Init.Logic <> :type_scope:x_'='_x not
R9100:9102 Coq.Init.Peano <> min syndef
R9104:9104 General <> m var
prf 9157:9163 <> min_min
R9193:9196 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9202:9205 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9198:9200 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9197:9197 General <> m var
R9201:9201 General <> n var
R9207:9209 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9206:9206 General <> m var
R9210:9210 General <> p var
R9182:9185 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9181:9181 General <> m var
R9186:9188 Coq.Init.Peano <> min syndef
R9192:9192 General <> p var
R9190:9190 General <> n var
R9305:9307 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9308:9310 Coq.Init.Peano <> min syndef
R9305:9307 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9308:9310 Coq.Init.Peano <> min syndef
R9343:9346 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9338:9340 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9348:9350 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9343:9346 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9338:9340 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9348:9350 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9423:9430 General <> min_zero thm
R9423:9430 General <> min_zero thm
R9423:9430 General <> min_zero thm
R9455:9457 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9458:9461 Coq.Init.Peano <> pred syndef
R9464:9466 Coq.Init.Peano <> min syndef
R9471:9471 Coq.Init.Datatypes <> S constr
R9455:9457 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9458:9461 Coq.Init.Peano <> pred syndef
R9464:9466 Coq.Init.Peano <> min syndef
R9471:9471 Coq.Init.Datatypes <> S constr
R9498:9505 General <> min_pred thm
R9498:9505 General <> min_pred thm
R9498:9505 General <> min_pred thm
R9539:9542 Coq.Init.Peano <> pred syndef
R9539:9542 Coq.Init.Peano <> pred syndef
prf 9585:9592 <> min_min2
R9615:9618 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9624:9627 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9629:9631 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9628:9628 General <> k var
R9632:9634 Coq.Init.Peano <> min syndef
R9638:9638 General <> n var
R9636:9636 General <> m var
R9620:9622 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9619:9619 General <> k var
R9623:9623 General <> n var
R9611:9613 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9610:9610 General <> k var
R9614:9614 General <> m var
R9697:9700 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9691:9694 Coq.Init.Peano <> pred syndef
R9701:9703 Coq.Init.Peano <> min syndef
R9697:9700 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9691:9694 Coq.Init.Peano <> pred syndef
R9701:9703 Coq.Init.Peano <> min syndef
prf 9762:9769 <> min_plus
R9796:9798 Coq.Init.Logic <> :type_scope:x_'='_x not
R9793:9794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9786:9788 Coq.Init.Peano <> min syndef
R9792:9792 General <> n var
R9790:9790 General <> m var
R9795:9795 General <> k var
R9799:9801 Coq.Init.Peano <> min syndef
R9811:9811 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9810:9810 General <> n var
R9812:9812 General <> k var
R9805:9805 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9804:9804 General <> m var
R9806:9806 General <> k var
R9907:9910 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9891:9893 Coq.Init.Peano <> min syndef
R9898:9898 Coq.Init.Datatypes <> S constr
R9903:9903 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9907:9910 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9891:9893 Coq.Init.Peano <> min syndef
R9898:9898 Coq.Init.Datatypes <> S constr
R9903:9903 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9925:9934 General <> min_is_min thm
R9947:9950 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9951:9953 Coq.Init.Peano <> min syndef
R9958:9958 Coq.Init.Datatypes <> S constr
R9962:9962 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9947:9950 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9951:9953 Coq.Init.Peano <> min syndef
R9958:9958 Coq.Init.Datatypes <> S constr
R9962:9962 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9978:9985 General <> min_min2 thm
R10047:10050 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10032:10034 Coq.Init.Peano <> min syndef
R10038:10038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10039:10039 Coq.Init.Datatypes <> S constr
R10047:10050 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10032:10034 Coq.Init.Peano <> min syndef
R10038:10038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10039:10039 Coq.Init.Datatypes <> S constr
R10067:10076 General <> min_is_min thm
R10090:10093 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10094:10096 Coq.Init.Peano <> min syndef
R10100:10100 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10101:10101 Coq.Init.Datatypes <> S constr
R10090:10093 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10094:10096 Coq.Init.Peano <> min syndef
R10100:10100 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10101:10101 Coq.Init.Datatypes <> S constr
R10121:10128 General <> min_min2 thm
prf 10161:10169 <> min_minus
R10196:10198 Coq.Init.Logic <> :type_scope:x_'='_x not
R10193:10194 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R10186:10188 Coq.Init.Peano <> min syndef
R10192:10192 General <> n var
R10190:10190 General <> m var
R10195:10195 General <> k var
R10199:10201 Coq.Init.Peano <> min syndef
R10211:10211 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R10210:10210 General <> n var
R10212:10212 General <> k var
R10205:10205 Coq.Init.Peano <> :nat_scope:x_'-'_x not
R10204:10204 General <> m var
R10206:10206 General <> k var
R10285:10292 General <> min_zero thm
R10285:10292 General <> min_zero thm
R10285:10292 General <> min_zero thm
prf 10335:10347 <> min_monotonic
R10379:10382 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10391:10394 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10404:10407 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10395:10397 Coq.Init.Peano <> min syndef
R10402:10403 General <> m2 var
R10399:10400 General <> m1 var
R10408:10410 Coq.Init.Peano <> min syndef
R10415:10416 General <> n2 var
R10412:10413 General <> n1 var
R10385:10388 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10383:10384 General <> m2 var
R10389:10390 General <> n2 var
R10373:10376 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10371:10372 General <> m1 var
R10377:10378 General <> n1 var
R10545:10548 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10537:10539 Coq.Init.Peano <> min syndef
R10549:10551 Coq.Init.Peano <> min syndef
R10545:10548 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10537:10539 Coq.Init.Peano <> min syndef
R10549:10551 Coq.Init.Peano <> min syndef
prf 10608:10621 <> decidable_nats
R10638:10640 Coq.Init.Datatypes <> nat ind
R10647:10650 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R10645:10645 Coq.Init.Logic <> :type_scope:x_'='_x not
R10644:10644 General <> m var
R10646:10646 General <> n var
R10652:10653 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R10651:10651 General <> m var
R10654:10654 General <> n var