-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLamSF_Normal.glob
2126 lines (2126 loc) · 87.6 KB
/
LamSF_Normal.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 c41b1164519b644c6aec31f2c86c88ac
FLamSF_Normal
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2018 General <> <> lib
R2036:2038 Coq.Arith.Max <> <> lib
R2057:2060 Test <> <> lib
R2078:2088 LamSF_Terms <> <> lib
R2106:2118 LamSF_Tactics <> <> lib
R2136:2158 LamSF_Substitution_term <> <> lib
R2176:2185 Components <> <> lib
R2203:2211 Compounds <> <> lib
R2229:2243 LamSF_reduction <> <> lib
ind 2278:2283 <> normal
constr 2307:2312 <> nf_ref
constr 2343:2347 <> nf_op
constr 2377:2382 <> nf_abs
constr 2425:2430 <> nf_app
R2287:2291 LamSF_Terms <> lamSF ind
R2326:2331 LamSF_Normal <> normal ind
R2334:2336 LamSF_Terms <> Ref constr
R2338:2338 LamSF_Normal <> n var
R2361:2366 LamSF_Normal <> normal ind
R2369:2370 LamSF_Terms <> Op constr
R2372:2372 LamSF_Normal <> o var
R2408:2413 LamSF_Normal <> normal ind
R2416:2418 LamSF_Terms <> Abs constr
R2420:2420 LamSF_Normal <> M var
R2396:2401 LamSF_Normal <> normal ind
R2403:2403 LamSF_Normal <> M var
R2535:2540 LamSF_Normal <> normal ind
R2543:2545 LamSF_Terms <> App constr
R2550:2551 LamSF_Normal <> M2 var
R2547:2548 LamSF_Normal <> M1 var
R2492:2495 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R2474:2479 Compounds <> status def
R2482:2484 LamSF_Terms <> App constr
R2489:2490 LamSF_Normal <> M2 var
R2486:2487 LamSF_Normal <> M1 var
R2496:2504 Compounds <> Reducible constr
R2461:2466 LamSF_Normal <> normal ind
R2468:2469 LamSF_Normal <> M2 var
R2448:2453 LamSF_Normal <> normal ind
R2455:2456 LamSF_Normal <> M1 var
R2577:2582 LamSF_Normal <> normal ind
prf 2593:2617 <> lift_rec_preserves_normal
R2656:2661 LamSF_Normal <> normal ind
R2663:2670 LamSF_Terms <> lift_rec def
R2676:2676 LamSF_Normal <> k var
R2674:2674 LamSF_Normal <> n var
R2672:2672 LamSF_Normal <> M var
R2631:2636 LamSF_Normal <> normal ind
R2638:2638 LamSF_Normal <> M var
R2736:2741 LamSF_Normal <> nf_app constr
R2784:2786 Coq.Init.Logic <> :type_scope:x_'='_x not
R2751:2756 Compounds <> status def
R2759:2766 LamSF_Terms <> lift_rec def
R2769:2771 LamSF_Terms <> App constr
R2787:2801 Compounds <> relocate_status def
R2803:2808 Compounds <> status def
R2811:2813 LamSF_Terms <> App constr
R2784:2786 Coq.Init.Logic <> :type_scope:x_'='_x not
R2751:2756 Compounds <> status def
R2759:2766 LamSF_Terms <> lift_rec def
R2769:2771 LamSF_Terms <> App constr
R2787:2801 Compounds <> relocate_status def
R2803:2808 Compounds <> status def
R2811:2813 LamSF_Terms <> App constr
R2838:2862 Compounds <> lift_rec_preserves_status thm
R2873:2880 LamSF_Terms <> lift_rec def
R2894:2901 LamSF_Terms <> lift_rec def
R2894:2901 LamSF_Terms <> lift_rec def
R2931:2945 Compounds <> relocate_status def
R2973:2978 Compounds <> status def
R2981:2983 LamSF_Terms <> App constr
R2973:2978 Compounds <> status def
R2981:2983 LamSF_Terms <> App constr
prf 3008:3015 <> normal_I
R3019:3024 LamSF_Normal <> normal ind
R3026:3029 Components <> i_op def
R3077:3082 LamSF_Normal <> nf_app constr
R3077:3082 LamSF_Normal <> nf_app constr
R3077:3082 LamSF_Normal <> nf_app constr
R3077:3082 LamSF_Normal <> nf_app constr
R3149:3156 LamSF_Normal <> normal_I thm
prf 3167:3179 <> normal_status
R3214:3217 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R3206:3211 Compounds <> status def
R3213:3213 LamSF_Normal <> M var
R3218:3226 Compounds <> Reducible constr
R3194:3199 LamSF_Normal <> normal ind
R3201:3201 LamSF_Normal <> M var
R3338:3343 Compounds <> status def
R3338:3343 Compounds <> status def
prf 3384:3394 <> normal_star
R3421:3426 LamSF_Normal <> normal ind
R3429:3432 Components <> star def
R3434:3434 LamSF_Normal <> M var
R3409:3414 LamSF_Normal <> normal ind
R3416:3416 LamSF_Normal <> M var
R3548:3553 LamSF_Normal <> nf_app constr
R3585:3590 LamSF_Normal <> nf_app constr
R3624:3629 LamSF_Normal <> nf_app constr
R3683:3690 Compounds <> compound def
R3668:3673 LamSF_Normal <> nf_app constr
R3668:3673 LamSF_Normal <> nf_app constr
R3668:3673 LamSF_Normal <> nf_app constr
R3668:3673 LamSF_Normal <> nf_app constr
prf 3719:3736 <> normal_component_l
R3762:3767 LamSF_Normal <> normal ind
R3770:3783 Components <> left_component def
R3785:3785 LamSF_Normal <> M var
R3750:3755 LamSF_Normal <> normal ind
R3757:3757 LamSF_Normal <> M var
R3892:3899 Compounds <> compound def
R3877:3882 LamSF_Normal <> nf_app constr
R3877:3882 LamSF_Normal <> nf_app constr
R3877:3882 LamSF_Normal <> nf_app constr
R3877:3882 LamSF_Normal <> nf_app constr
R3877:3882 LamSF_Normal <> nf_app constr
R3877:3882 LamSF_Normal <> nf_app constr
prf 3925:3942 <> normal_component_r
R3968:3973 LamSF_Normal <> normal ind
R3976:3990 Components <> right_component def
R3992:3992 LamSF_Normal <> M var
R3956:3961 LamSF_Normal <> normal ind
R3963:3963 LamSF_Normal <> M var
R4076:4086 LamSF_Normal <> normal_star thm
def 4108:4118 <> irreducible
R4127:4133 LamSF_Tactics <> termred def
R4160:4164 Coq.Init.Logic <> False ind
R4149:4151 LamSF_Normal <> red var
R4155:4155 LamSF_Normal <> N var
R4153:4153 LamSF_Normal <> M var
prf 4175:4189 <> ref_irreducible
R4203:4213 LamSF_Normal <> irreducible def
R4223:4232 LamSF_reduction <> lamSF_red1 ind
R4216:4218 LamSF_Terms <> Ref constr
R4220:4220 LamSF_Normal <> n var
prf 5038:5064 <> Reducible_implies_reducible
R5103:5109 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5111:5112 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5113:5122 LamSF_reduction <> lamSF_red1 ind
R5126:5126 LamSF_Normal <> N var
R5124:5124 LamSF_Normal <> M var
R5087:5089 Coq.Init.Logic <> :type_scope:x_'='_x not
R5079:5084 Compounds <> status def
R5086:5086 LamSF_Normal <> M var
R5090:5098 Compounds <> Reducible constr
R5266:5271 Compounds <> status def
R5266:5271 Compounds <> status def
R5294:5300 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5302:5303 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5304:5313 LamSF_reduction <> lamSF_red1 ind
R5317:5317 LamSF_Normal <> N var
R5294:5300 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5302:5303 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5304:5313 LamSF_reduction <> lamSF_red1 ind
R5317:5317 LamSF_Normal <> N var
R5360:5362 LamSF_Terms <> Abs constr
R5360:5362 LamSF_Terms <> Abs constr
R5466:5469 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5454:5456 Coq.Init.Logic <> :type_scope:x_'='_x not
R5445:5450 Compounds <> status def
R5457:5465 Compounds <> Reducible constr
R5491:5502 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5479:5481 Coq.Init.Logic <> :type_scope:x_'='_x not
R5470:5475 Compounds <> status def
R5482:5490 Compounds <> Reducible constr
R5503:5503 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5531:5543 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5504:5510 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5512:5513 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5523:5525 Coq.Init.Logic <> :type_scope:x_'='_x not
R5514:5519 Compounds <> status def
R5526:5528 Compounds <> Lam constr
R5530:5530 LamSF_Normal <> i var
R5561:5572 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5553:5555 Coq.Init.Logic <> :type_scope:x_'='_x not
R5544:5549 Compounds <> status def
R5556:5560 Compounds <> Lazy1 constr
R5593:5604 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5582:5584 Coq.Init.Logic <> :type_scope:x_'='_x not
R5573:5578 Compounds <> status def
R5585:5592 Compounds <> Unary_op constr
R5605:5605 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5643:5656 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5691:5691 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5628:5631 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5615:5617 Coq.Init.Logic <> :type_scope:x_'='_x not
R5606:5611 Compounds <> status def
R5618:5627 Compounds <> Binary_op2 constr
R5632:5639 Compounds <> compound def
R5674:5677 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5666:5668 Coq.Init.Logic <> :type_scope:x_'='_x not
R5657:5662 Compounds <> status def
R5669:5673 Compounds <> Eager constr
R5678:5687 Compounds <> factorable def
R5466:5469 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5454:5456 Coq.Init.Logic <> :type_scope:x_'='_x not
R5445:5450 Compounds <> status def
R5457:5465 Compounds <> Reducible constr
R5491:5502 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5479:5481 Coq.Init.Logic <> :type_scope:x_'='_x not
R5470:5475 Compounds <> status def
R5482:5490 Compounds <> Reducible constr
R5503:5503 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5531:5543 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5504:5510 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5512:5513 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5523:5525 Coq.Init.Logic <> :type_scope:x_'='_x not
R5514:5519 Compounds <> status def
R5526:5528 Compounds <> Lam constr
R5530:5530 LamSF_Normal <> i var
R5561:5572 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5553:5555 Coq.Init.Logic <> :type_scope:x_'='_x not
R5544:5549 Compounds <> status def
R5556:5560 Compounds <> Lazy1 constr
R5593:5604 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5582:5584 Coq.Init.Logic <> :type_scope:x_'='_x not
R5573:5578 Compounds <> status def
R5585:5592 Compounds <> Unary_op constr
R5605:5605 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5643:5656 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5691:5691 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5628:5631 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5615:5617 Coq.Init.Logic <> :type_scope:x_'='_x not
R5606:5611 Compounds <> status def
R5618:5627 Compounds <> Binary_op2 constr
R5632:5639 Compounds <> compound def
R5674:5677 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5666:5668 Coq.Init.Logic <> :type_scope:x_'='_x not
R5657:5662 Compounds <> status def
R5669:5673 Compounds <> Eager constr
R5678:5687 Compounds <> factorable def
R5702:5711 Compounds <> factorable def
R5714:5721 Compounds <> compound def
R5757:5762 Compounds <> status def
R5795:5800 Compounds <> status def
R5757:5762 Compounds <> status def
R5795:5800 Compounds <> status def
R5795:5800 Compounds <> status def
R5795:5800 Compounds <> status def
R5894:5896 LamSF_Terms <> App constr
R5894:5896 LamSF_Terms <> App constr
R5975:5977 LamSF_Terms <> App constr
R5975:5977 LamSF_Terms <> App constr
R6020:6026 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6029:6030 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6033:6035 Coq.Init.Logic <> :type_scope:x_'='_x not
R6036:6038 LamSF_Terms <> Abs constr
R6040:6041 LamSF_Normal <> M0 var
R6020:6026 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6029:6030 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6033:6035 Coq.Init.Logic <> :type_scope:x_'='_x not
R6036:6038 LamSF_Terms <> Abs constr
R6040:6041 LamSF_Normal <> M0 var
R6055:6064 Compounds <> lam_is_abs thm
R6221:6226 Compounds <> status def
R6221:6226 Compounds <> status def
R6342:6347 Compounds <> status def
R6370:6375 Compounds <> status def
R6342:6347 Compounds <> status def
R6370:6375 Compounds <> status def
R6370:6375 Compounds <> status def
R6370:6375 Compounds <> status def
R6370:6375 Compounds <> status def
R6370:6375 Compounds <> status def
R6370:6375 Compounds <> status def
R6408:6413 Compounds <> status def
R6436:6441 Compounds <> status def
R6408:6413 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6436:6441 Compounds <> status def
R6474:6479 Compounds <> status def
R6474:6479 Compounds <> status def
R6508:6513 Compounds <> status def
R6538:6543 Compounds <> status def
R6508:6513 Compounds <> status def
R6538:6543 Compounds <> status def
R6538:6543 Compounds <> status def
R6538:6543 Compounds <> status def
R6538:6543 Compounds <> status def
R6538:6543 Compounds <> status def
R6573:6578 Compounds <> status def
R6600:6605 Compounds <> status def
R6573:6578 Compounds <> status def
R6600:6605 Compounds <> status def
R6600:6605 Compounds <> status def
R6600:6605 Compounds <> status def
R6600:6605 Compounds <> status def
R6600:6605 Compounds <> status def
R6600:6605 Compounds <> status def
R6626:6631 Compounds <> status def
R6626:6631 Compounds <> status def
R6652:6657 Compounds <> status def
R6679:6684 Compounds <> status def
R6652:6657 Compounds <> status def
R6798:6803 Compounds <> status def
R6822:6827 Compounds <> status def
R6798:6803 Compounds <> status def
R6822:6827 Compounds <> status def
R6822:6827 Compounds <> status def
R6932:6937 Compounds <> status def
R6956:6961 Compounds <> status def
R6932:6937 Compounds <> status def
R6956:6961 Compounds <> status def
R6956:6961 Compounds <> status def
R7088:7093 Compounds <> status def
R7088:7093 Compounds <> status def
R7088:7093 Compounds <> status def
R7115:7121 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7123:7124 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7127:7129 Coq.Init.Logic <> :type_scope:x_'='_x not
R7130:7131 LamSF_Terms <> Op constr
R7133:7133 LamSF_Normal <> o var
R7115:7121 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7123:7124 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7127:7129 Coq.Init.Logic <> :type_scope:x_'='_x not
R7130:7131 LamSF_Terms <> Op constr
R7133:7133 LamSF_Normal <> o var
R7175:7180 Compounds <> status def
R7175:7180 Compounds <> status def
R7231:7236 Compounds <> status def
R7263:7268 Compounds <> status def
R7231:7236 Compounds <> status def
R7263:7268 Compounds <> status def
R7263:7268 Compounds <> status def
R7317:7320 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7310:7312 Coq.Init.Logic <> :type_scope:x_'='_x not
R7313:7314 LamSF_Terms <> Op constr
R7323:7326 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7327:7328 LamSF_Terms <> Op constr
R7317:7320 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7310:7312 Coq.Init.Logic <> :type_scope:x_'='_x not
R7313:7314 LamSF_Terms <> Op constr
R7323:7326 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7327:7328 LamSF_Terms <> Op constr
R7396:7434 Compounds <> factorable_implies_compound_or_operator thm
R7396:7434 Compounds <> factorable_implies_compound_or_operator thm
R7493:7495 Coq.Init.Logic <> :type_scope:x_'='_x not
R7484:7489 Compounds <> status def
R7496:7506 Compounds <> Ternary_op1 constr
R7493:7495 Coq.Init.Logic <> :type_scope:x_'='_x not
R7484:7489 Compounds <> status def
R7496:7506 Compounds <> Ternary_op1 constr
R7524:7529 Compounds <> status def
R7554:7559 Compounds <> status def
R7524:7529 Compounds <> status def
R7554:7559 Compounds <> status def
R7554:7559 Compounds <> status def
R7554:7559 Compounds <> status def
R7554:7559 Compounds <> status def
R7596:7601 Compounds <> status def
R7621:7626 Compounds <> status def
R7596:7601 Compounds <> status def
R7621:7626 Compounds <> status def
R7621:7626 Compounds <> status def
R7621:7626 Compounds <> status def
R7621:7626 Compounds <> status def
R7621:7626 Compounds <> status def
R7621:7626 Compounds <> status def
R7656:7661 Compounds <> status def
R7656:7661 Compounds <> status def
R7682:7687 Compounds <> status def
R7682:7687 Compounds <> status def
R7700:7738 Compounds <> factorable_implies_compound_or_operator thm
R7700:7738 Compounds <> factorable_implies_compound_or_operator thm
R7835:7838 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7826:7828 Coq.Init.Logic <> :type_scope:x_'='_x not
R7829:7830 LamSF_Terms <> Op constr
R7832:7834 LamSF_Terms <> Sop constr
R7841:7844 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7845:7846 LamSF_Terms <> Op constr
R7848:7850 LamSF_Terms <> Sop constr
R7835:7838 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7826:7828 Coq.Init.Logic <> :type_scope:x_'='_x not
R7829:7830 LamSF_Terms <> Op constr
R7832:7834 LamSF_Terms <> Sop constr
R7841:7844 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7845:7846 LamSF_Terms <> Op constr
R7848:7850 LamSF_Terms <> Sop constr
R7930:7933 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7921:7923 Coq.Init.Logic <> :type_scope:x_'='_x not
R7924:7925 LamSF_Terms <> Op constr
R7927:7929 LamSF_Terms <> Aop constr
R7936:7939 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7940:7941 LamSF_Terms <> Op constr
R7943:7945 LamSF_Terms <> Aop constr
R7930:7933 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7921:7923 Coq.Init.Logic <> :type_scope:x_'='_x not
R7924:7925 LamSF_Terms <> Op constr
R7927:7929 LamSF_Terms <> Aop constr
R7936:7939 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7940:7941 LamSF_Terms <> Op constr
R7943:7945 LamSF_Terms <> Aop constr
R8025:8028 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8016:8018 Coq.Init.Logic <> :type_scope:x_'='_x not
R8019:8020 LamSF_Terms <> Op constr
R8022:8024 LamSF_Terms <> Kop constr
R8031:8034 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8035:8036 LamSF_Terms <> Op constr
R8038:8040 LamSF_Terms <> Kop constr
R8025:8028 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8016:8018 Coq.Init.Logic <> :type_scope:x_'='_x not
R8019:8020 LamSF_Terms <> Op constr
R8022:8024 LamSF_Terms <> Kop constr
R8031:8034 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8035:8036 LamSF_Terms <> Op constr
R8038:8040 LamSF_Terms <> Kop constr
R8120:8123 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8111:8113 Coq.Init.Logic <> :type_scope:x_'='_x not
R8114:8115 LamSF_Terms <> Op constr
R8117:8119 LamSF_Terms <> Eop constr
R8126:8129 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8130:8131 LamSF_Terms <> Op constr
R8133:8135 LamSF_Terms <> Eop constr
R8120:8123 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8111:8113 Coq.Init.Logic <> :type_scope:x_'='_x not
R8114:8115 LamSF_Terms <> Op constr
R8117:8119 LamSF_Terms <> Eop constr
R8126:8129 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8130:8131 LamSF_Terms <> Op constr
R8133:8135 LamSF_Terms <> Eop constr
R8215:8218 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8206:8208 Coq.Init.Logic <> :type_scope:x_'='_x not
R8209:8210 LamSF_Terms <> Op constr
R8212:8214 LamSF_Terms <> Gop constr
R8221:8224 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8225:8226 LamSF_Terms <> Op constr
R8228:8230 LamSF_Terms <> Gop constr
R8215:8218 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8206:8208 Coq.Init.Logic <> :type_scope:x_'='_x not
R8209:8210 LamSF_Terms <> Op constr
R8212:8214 LamSF_Terms <> Gop constr
R8221:8224 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8225:8226 LamSF_Terms <> Op constr
R8228:8230 LamSF_Terms <> Gop constr
R8310:8313 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8301:8303 Coq.Init.Logic <> :type_scope:x_'='_x not
R8304:8305 LamSF_Terms <> Op constr
R8307:8309 LamSF_Terms <> Qop constr
R8316:8319 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8320:8321 LamSF_Terms <> Op constr
R8323:8325 LamSF_Terms <> Qop constr
R8310:8313 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8301:8303 Coq.Init.Logic <> :type_scope:x_'='_x not
R8304:8305 LamSF_Terms <> Op constr
R8307:8309 LamSF_Terms <> Qop constr
R8316:8319 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8320:8321 LamSF_Terms <> Op constr
R8323:8325 LamSF_Terms <> Qop constr
R8405:8408 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8396:8398 Coq.Init.Logic <> :type_scope:x_'='_x not
R8399:8400 LamSF_Terms <> Op constr
R8402:8404 LamSF_Terms <> Uop constr
R8411:8414 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8415:8416 LamSF_Terms <> Op constr
R8418:8420 LamSF_Terms <> Uop constr
R8405:8408 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8396:8398 Coq.Init.Logic <> :type_scope:x_'='_x not
R8399:8400 LamSF_Terms <> Op constr
R8402:8404 LamSF_Terms <> Uop constr
R8411:8414 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8415:8416 LamSF_Terms <> Op constr
R8418:8420 LamSF_Terms <> Uop constr
R8500:8503 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8491:8493 Coq.Init.Logic <> :type_scope:x_'='_x not
R8494:8495 LamSF_Terms <> Op constr
R8497:8499 LamSF_Terms <> Yop constr
R8506:8509 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8510:8511 LamSF_Terms <> Op constr
R8513:8515 LamSF_Terms <> Yop constr
R8500:8503 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8491:8493 Coq.Init.Logic <> :type_scope:x_'='_x not
R8494:8495 LamSF_Terms <> Op constr
R8497:8499 LamSF_Terms <> Yop constr
R8506:8509 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8510:8511 LamSF_Terms <> Op constr
R8513:8515 LamSF_Terms <> Yop constr
R8590:8595 Compounds <> status def
R8616:8621 Compounds <> status def
R8590:8595 Compounds <> status def
R8616:8621 Compounds <> status def
R8616:8621 Compounds <> status def
R8683:8686 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8677:8679 Coq.Init.Logic <> :type_scope:x_'='_x not
R8680:8682 LamSF_Terms <> Sop constr
R8688:8691 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8692:8694 LamSF_Terms <> Sop constr
R8683:8686 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8677:8679 Coq.Init.Logic <> :type_scope:x_'='_x not
R8680:8682 LamSF_Terms <> Sop constr
R8688:8691 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8692:8694 LamSF_Terms <> Sop constr
R8767:8770 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8763:8764 LamSF_Terms <> Op constr
R8771:8772 LamSF_Terms <> Op constr
R8774:8776 LamSF_Terms <> Sop constr
R8767:8770 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8763:8764 LamSF_Terms <> Op constr
R8771:8772 LamSF_Terms <> Op constr
R8774:8776 LamSF_Terms <> Sop constr
R8847:8850 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8841:8843 Coq.Init.Logic <> :type_scope:x_'='_x not
R8844:8846 LamSF_Terms <> Aop constr
R8852:8855 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8856:8858 LamSF_Terms <> Aop constr
R8847:8850 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8841:8843 Coq.Init.Logic <> :type_scope:x_'='_x not
R8844:8846 LamSF_Terms <> Aop constr
R8852:8855 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8856:8858 LamSF_Terms <> Aop constr
R8932:8935 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8928:8929 LamSF_Terms <> Op constr
R8936:8937 LamSF_Terms <> Op constr
R8939:8941 LamSF_Terms <> Aop constr
R8932:8935 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R8928:8929 LamSF_Terms <> Op constr
R8936:8937 LamSF_Terms <> Op constr
R8939:8941 LamSF_Terms <> Aop constr
R9012:9015 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9006:9008 Coq.Init.Logic <> :type_scope:x_'='_x not
R9009:9011 LamSF_Terms <> Kop constr
R9017:9020 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9021:9023 LamSF_Terms <> Kop constr
R9012:9015 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9006:9008 Coq.Init.Logic <> :type_scope:x_'='_x not
R9009:9011 LamSF_Terms <> Kop constr
R9017:9020 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9021:9023 LamSF_Terms <> Kop constr
R9097:9100 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9093:9094 LamSF_Terms <> Op constr
R9101:9102 LamSF_Terms <> Op constr
R9104:9106 LamSF_Terms <> Kop constr
R9097:9100 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9093:9094 LamSF_Terms <> Op constr
R9101:9102 LamSF_Terms <> Op constr
R9104:9106 LamSF_Terms <> Kop constr
R9177:9180 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9171:9173 Coq.Init.Logic <> :type_scope:x_'='_x not
R9174:9176 LamSF_Terms <> Eop constr
R9182:9185 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9186:9188 LamSF_Terms <> Eop constr
R9177:9180 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9171:9173 Coq.Init.Logic <> :type_scope:x_'='_x not
R9174:9176 LamSF_Terms <> Eop constr
R9182:9185 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9186:9188 LamSF_Terms <> Eop constr
R9262:9265 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9258:9259 LamSF_Terms <> Op constr
R9266:9267 LamSF_Terms <> Op constr
R9269:9271 LamSF_Terms <> Eop constr
R9262:9265 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9258:9259 LamSF_Terms <> Op constr
R9266:9267 LamSF_Terms <> Op constr
R9269:9271 LamSF_Terms <> Eop constr
R9342:9345 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9336:9338 Coq.Init.Logic <> :type_scope:x_'='_x not
R9339:9341 LamSF_Terms <> Gop constr
R9347:9350 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9351:9353 LamSF_Terms <> Gop constr
R9342:9345 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9336:9338 Coq.Init.Logic <> :type_scope:x_'='_x not
R9339:9341 LamSF_Terms <> Gop constr
R9347:9350 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9351:9353 LamSF_Terms <> Gop constr
R9427:9430 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9423:9424 LamSF_Terms <> Op constr
R9431:9432 LamSF_Terms <> Op constr
R9434:9436 LamSF_Terms <> Gop constr
R9427:9430 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9423:9424 LamSF_Terms <> Op constr
R9431:9432 LamSF_Terms <> Op constr
R9434:9436 LamSF_Terms <> Gop constr
R9507:9510 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9501:9503 Coq.Init.Logic <> :type_scope:x_'='_x not
R9504:9506 LamSF_Terms <> Qop constr
R9512:9515 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9516:9518 LamSF_Terms <> Qop constr
R9507:9510 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9501:9503 Coq.Init.Logic <> :type_scope:x_'='_x not
R9504:9506 LamSF_Terms <> Qop constr
R9512:9515 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9516:9518 LamSF_Terms <> Qop constr
R9592:9595 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9588:9589 LamSF_Terms <> Op constr
R9596:9597 LamSF_Terms <> Op constr
R9599:9601 LamSF_Terms <> Qop constr
R9592:9595 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9588:9589 LamSF_Terms <> Op constr
R9596:9597 LamSF_Terms <> Op constr
R9599:9601 LamSF_Terms <> Qop constr
R9672:9675 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9666:9668 Coq.Init.Logic <> :type_scope:x_'='_x not
R9669:9671 LamSF_Terms <> Uop constr
R9677:9680 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9681:9683 LamSF_Terms <> Uop constr
R9672:9675 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9666:9668 Coq.Init.Logic <> :type_scope:x_'='_x not
R9669:9671 LamSF_Terms <> Uop constr
R9677:9680 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9681:9683 LamSF_Terms <> Uop constr
R9757:9760 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9753:9754 LamSF_Terms <> Op constr
R9761:9762 LamSF_Terms <> Op constr
R9764:9766 LamSF_Terms <> Uop constr
R9757:9760 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9753:9754 LamSF_Terms <> Op constr
R9761:9762 LamSF_Terms <> Op constr
R9764:9766 LamSF_Terms <> Uop constr
R9837:9840 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9831:9833 Coq.Init.Logic <> :type_scope:x_'='_x not
R9834:9836 LamSF_Terms <> Yop constr
R9842:9845 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9846:9848 LamSF_Terms <> Yop constr
R9837:9840 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9831:9833 Coq.Init.Logic <> :type_scope:x_'='_x not
R9834:9836 LamSF_Terms <> Yop constr
R9842:9845 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9846:9848 LamSF_Terms <> Yop constr
R9922:9925 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9918:9919 LamSF_Terms <> Op constr
R9926:9927 LamSF_Terms <> Op constr
R9929:9931 LamSF_Terms <> Yop constr
R9922:9925 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R9918:9919 LamSF_Terms <> Op constr
R9926:9927 LamSF_Terms <> Op constr
R9929:9931 LamSF_Terms <> Yop constr
R10027:10032 Compounds <> status def
R10052:10057 Compounds <> status def
R10027:10032 Compounds <> status def
R10052:10057 Compounds <> status def
R10052:10057 Compounds <> status def
prf 10081:10098 <> active_irreducible
R10238:10248 LamSF_Normal <> irreducible def
R10252:10261 LamSF_reduction <> lamSF_red1 ind
R10250:10250 LamSF_Normal <> M var
R10192:10202 LamSF_Normal <> irreducible def
R10224:10233 LamSF_reduction <> lamSF_red1 ind
R10205:10219 Components <> right_component def
R10221:10221 LamSF_Normal <> M var
R10146:10156 LamSF_Normal <> irreducible def
R10177:10186 LamSF_reduction <> lamSF_red1 ind
R10159:10172 Components <> left_component def
R10174:10174 LamSF_Normal <> M var
R10130:10132 Coq.Init.Logic <> :type_scope:x_'='_x not
R10122:10127 Compounds <> status def
R10129:10129 LamSF_Normal <> M var
R10133:10138 Compounds <> Active constr
R10140:10140 LamSF_Normal <> i var
R10412:10417 Compounds <> status def
R10412:10417 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10515:10520 Compounds <> status def
R10673:10682 Compounds <> factorable def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10707:10712 Compounds <> status def
R10756:10763 Compounds <> compound def
R10788:10793 Compounds <> status def
R10788:10793 Compounds <> status def
R10837:10846 Compounds <> factorable def
R10871:10876 Compounds <> status def
R10871:10876 Compounds <> status def
R10958:10965 Compounds <> compound def
R10990:10995 Compounds <> status def
R10990:10995 Compounds <> status def
R11076:11083 Compounds <> compound def
R11108:11113 Compounds <> status def
R11108:11113 Compounds <> status def
R11147:11156 Compounds <> factorable def
R11181:11186 Compounds <> status def
R11181:11186 Compounds <> status def
R11220:11229 Compounds <> factorable def
R11254:11259 Compounds <> status def
R11254:11259 Compounds <> status def
R11293:11302 Compounds <> factorable def
R11327:11332 Compounds <> status def
R11327:11332 Compounds <> status def
R11366:11375 Compounds <> factorable def
R11400:11405 Compounds <> status def
R11400:11405 Compounds <> status def
R11439:11448 Compounds <> factorable def
R11473:11478 Compounds <> status def
R11473:11478 Compounds <> status def
R11512:11521 Compounds <> factorable def
R11546:11551 Compounds <> status def
R11546:11551 Compounds <> status def
R11585:11594 Compounds <> factorable def
R11619:11624 Compounds <> status def
R11619:11624 Compounds <> status def
R11658:11667 Compounds <> factorable def
R11692:11697 Compounds <> status def
R11692:11697 Compounds <> status def
prf 11726:11740 <> abs_irreducible
R11784:11794 LamSF_Normal <> irreducible def
R11804:11813 LamSF_reduction <> lamSF_red1 ind
R11797:11799 LamSF_Terms <> Abs constr
R11801:11801 LamSF_Normal <> M var
R11755:11765 LamSF_Normal <> irreducible def
R11769:11778 LamSF_reduction <> lamSF_red1 ind
R11767:11767 LamSF_Normal <> M var
prf 11880:11900 <> normal_is_irreducible
R11926:11936 LamSF_Normal <> irreducible def
R11940:11949 LamSF_reduction <> lamSF_red1 ind
R11938:11938 LamSF_Normal <> M var
R11914:11919 LamSF_Normal <> normal ind
R11921:11921 LamSF_Normal <> M var
R12017:12031 LamSF_Normal <> ref_irreducible thm
R12073:12087 LamSF_Normal <> abs_irreducible thm
R12107:12107 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12177:12182 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12108:12114 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R12116:12117 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R12147:12150 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12136:12138 Coq.Init.Logic <> :type_scope:x_'='_x not
R12118:12123 Compounds <> status def
R12126:12128 LamSF_Terms <> App constr
R12139:12144 Compounds <> Active constr
R12146:12146 LamSF_Normal <> i var
R12169:12171 Coq.Init.Logic <> :type_scope:x_'='_x not
R12151:12156 Compounds <> status def
R12159:12161 LamSF_Terms <> App constr
R12172:12174 Compounds <> Lam constr
R12176:12176 LamSF_Normal <> i var
R12214:12217 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12201:12203 Coq.Init.Logic <> :type_scope:x_'='_x not
R12183:12188 Compounds <> status def
R12191:12193 LamSF_Terms <> App constr
R12204:12213 Compounds <> Ternary_op constr
R12250:12253 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12236:12239 Coq.Init.Logic <> :type_scope:x_'='_x not
R12218:12223 Compounds <> status def
R12226:12228 LamSF_Terms <> App constr
R12240:12249 Compounds <> Binary_op0 constr
R12285:12288 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12272:12274 Coq.Init.Logic <> :type_scope:x_'='_x not
R12254:12259 Compounds <> status def
R12262:12264 LamSF_Terms <> App constr
R12275:12284 Compounds <> Binary_op2 constr
R12321:12325 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12307:12310 Coq.Init.Logic <> :type_scope:x_'='_x not
R12289:12294 Compounds <> status def
R12297:12299 LamSF_Terms <> App constr
R12311:12320 Compounds <> Binary_op1 constr
R12359:12363 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12344:12347 Coq.Init.Logic <> :type_scope:x_'='_x not
R12326:12331 Compounds <> status def
R12334:12336 LamSF_Terms <> App constr
R12348:12358 Compounds <> Ternary_op1 constr
R12394:12398 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12382:12385 Coq.Init.Logic <> :type_scope:x_'='_x not
R12364:12369 Compounds <> status def
R12372:12374 LamSF_Terms <> App constr
R12386:12393 Compounds <> Unary_op constr
R12425:12429 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12417:12419 Coq.Init.Logic <> :type_scope:x_'='_x not
R12399:12404 Compounds <> status def
R12407:12409 LamSF_Terms <> App constr
R12420:12424 Compounds <> Lazy2 constr
R12456:12460 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12448:12450 Coq.Init.Logic <> :type_scope:x_'='_x not
R12430:12435 Compounds <> status def
R12438:12440 LamSF_Terms <> App constr
R12451:12455 Compounds <> Lazy1 constr
R12488:12492 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12479:12481 Coq.Init.Logic <> :type_scope:x_'='_x not
R12461:12466 Compounds <> status def
R12469:12471 LamSF_Terms <> App constr
R12482:12487 Compounds <> Eager2 constr
R12511:12513 Coq.Init.Logic <> :type_scope:x_'='_x not
R12493:12498 Compounds <> status def
R12501:12503 LamSF_Terms <> App constr
R12514:12518 Compounds <> Eager constr
R12107:12107 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12177:12182 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12108:12114 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R12116:12117 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R12147:12150 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12136:12138 Coq.Init.Logic <> :type_scope:x_'='_x not
R12118:12123 Compounds <> status def
R12126:12128 LamSF_Terms <> App constr
R12139:12144 Compounds <> Active constr
R12146:12146 LamSF_Normal <> i var
R12169:12171 Coq.Init.Logic <> :type_scope:x_'='_x not
R12151:12156 Compounds <> status def
R12159:12161 LamSF_Terms <> App constr
R12172:12174 Compounds <> Lam constr
R12176:12176 LamSF_Normal <> i var
R12214:12217 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12201:12203 Coq.Init.Logic <> :type_scope:x_'='_x not
R12183:12188 Compounds <> status def
R12191:12193 LamSF_Terms <> App constr
R12204:12213 Compounds <> Ternary_op constr
R12250:12253 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12236:12239 Coq.Init.Logic <> :type_scope:x_'='_x not
R12218:12223 Compounds <> status def
R12226:12228 LamSF_Terms <> App constr
R12240:12249 Compounds <> Binary_op0 constr
R12285:12288 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12272:12274 Coq.Init.Logic <> :type_scope:x_'='_x not
R12254:12259 Compounds <> status def
R12262:12264 LamSF_Terms <> App constr
R12275:12284 Compounds <> Binary_op2 constr
R12321:12325 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12307:12310 Coq.Init.Logic <> :type_scope:x_'='_x not
R12289:12294 Compounds <> status def
R12297:12299 LamSF_Terms <> App constr
R12311:12320 Compounds <> Binary_op1 constr
R12359:12363 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12344:12347 Coq.Init.Logic <> :type_scope:x_'='_x not
R12326:12331 Compounds <> status def
R12334:12336 LamSF_Terms <> App constr
R12348:12358 Compounds <> Ternary_op1 constr
R12394:12398 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12382:12385 Coq.Init.Logic <> :type_scope:x_'='_x not
R12364:12369 Compounds <> status def
R12372:12374 LamSF_Terms <> App constr
R12386:12393 Compounds <> Unary_op constr
R12425:12429 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12417:12419 Coq.Init.Logic <> :type_scope:x_'='_x not
R12399:12404 Compounds <> status def
R12407:12409 LamSF_Terms <> App constr
R12420:12424 Compounds <> Lazy2 constr
R12456:12460 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12448:12450 Coq.Init.Logic <> :type_scope:x_'='_x not
R12430:12435 Compounds <> status def
R12438:12440 LamSF_Terms <> App constr
R12451:12455 Compounds <> Lazy1 constr
R12488:12492 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12479:12481 Coq.Init.Logic <> :type_scope:x_'='_x not
R12461:12466 Compounds <> status def
R12469:12471 LamSF_Terms <> App constr
R12482:12487 Compounds <> Eager2 constr
R12511:12513 Coq.Init.Logic <> :type_scope:x_'='_x not
R12493:12498 Compounds <> status def
R12501:12503 LamSF_Terms <> App constr
R12514:12518 Compounds <> Eager constr
R12534:12539 Compounds <> status def
R12542:12544 LamSF_Terms <> App constr
R12534:12539 Compounds <> status def
R12542:12544 LamSF_Terms <> App constr
R12631:12648 LamSF_Normal <> active_irreducible thm
R12679:12684 Compounds <> status def
R12704:12709 Compounds <> status def
R12679:12684 Compounds <> status def
R12704:12709 Compounds <> status def
R12704:12709 Compounds <> status def
R12780:12785 Compounds <> status def
R12805:12810 Compounds <> status def
R12780:12785 Compounds <> status def
R12805:12810 Compounds <> status def
R12805:12810 Compounds <> status def
R12881:12886 Compounds <> status def
R12906:12911 Compounds <> status def
R12881:12886 Compounds <> status def
R12906:12911 Compounds <> status def
R12906:12911 Compounds <> status def
R12982:12987 Compounds <> status def
R13007:13012 Compounds <> status def
R12982:12987 Compounds <> status def
R13007:13012 Compounds <> status def
R13007:13012 Compounds <> status def
R13083:13088 Compounds <> status def
R13108:13113 Compounds <> status def
R13083:13088 Compounds <> status def
R13108:13113 Compounds <> status def
R13108:13113 Compounds <> status def
R13233:13238 Compounds <> status def
R13233:13238 Compounds <> status def
R13259:13264 Compounds <> status def
R13259:13264 Compounds <> status def
R13299:13304 Compounds <> status def
R13323:13328 Compounds <> status def
R13348:13353 Compounds <> status def
R13299:13304 Compounds <> status def
R13323:13328 Compounds <> status def
R13323:13328 Compounds <> status def
R13323:13328 Compounds <> status def
R13323:13328 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13348:13353 Compounds <> status def
R13577:13582 Compounds <> status def
R13577:13582 Compounds <> status def
R13606:13611 Compounds <> status def
R13606:13611 Compounds <> status def
R13725:13730 Compounds <> status def
R13760:13765 Compounds <> status def
R13725:13730 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13725:13730 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13725:13730 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13760:13765 Compounds <> status def
R13802:13807 Compounds <> status def
R13802:13807 Compounds <> status def
R13863:13868 Compounds <> status def
R13863:13868 Compounds <> status def