forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LamSF_reduction.glob
894 lines (894 loc) · 38 KB
/
LamSF_reduction.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
DIGEST 60dc1e57d18fa3a24f93756b57e85544
FLamSF_reduction
R1992:1996 Coq.Arith.Arith <> <> lib
R2014:2016 Coq.Arith.Max <> <> lib
R2035:2038 Test <> <> lib
R2056:2062 General <> <> lib
R2081:2091 LamSF_Terms <> <> lib
R2109:2121 LamSF_Tactics <> <> lib
R2139:2161 LamSF_Substitution_term <> <> lib
R2179:2192 Beta_Reduction <> <> lib
R2210:2225 LamSF_Confluence <> <> lib
R2243:2254 SF_reduction <> <> lib
R2272:2276 Coq.omega.Omega <> <> lib
ind 2314:2323 <> lamSF_red1
constr 2358:2371 <> appl_lamSF_red
constr 2487:2500 <> appr_lamSF_red
constr 2616:2628 <> abs_lamSF_red
constr 2696:2709 <> beta_lamSF_red
constr 2798:2808 <> s_lamSF_red
constr 2961:2974 <> f_op_lamSF_red
constr 3065:3084 <> f_compound_lamSF_red
R2332:2335 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2341:2344 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2336:2340 LamSF_Terms <> lamSF ind
R2327:2331 LamSF_Terms <> lamSF ind
R2406:2448 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2449:2458 LamSF_reduction <> lamSF_red1 ind
R2471:2473 LamSF_Terms <> App constr
R2478:2478 LamSF_reduction <> N var
R2475:2476 LamSF_reduction <> M' var
R2461:2463 LamSF_Terms <> App constr
R2467:2467 LamSF_reduction <> N var
R2465:2465 LamSF_reduction <> M var
R2391:2400 LamSF_reduction <> lamSF_red1 ind
R2404:2405 LamSF_reduction <> M' var
R2402:2402 LamSF_reduction <> M var
R2535:2577 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2578:2587 LamSF_reduction <> lamSF_red1 ind
R2600:2602 LamSF_Terms <> App constr
R2606:2607 LamSF_reduction <> N' var
R2604:2604 LamSF_reduction <> M var
R2590:2592 LamSF_Terms <> App constr
R2596:2596 LamSF_reduction <> N var
R2594:2594 LamSF_reduction <> M var
R2520:2529 LamSF_reduction <> lamSF_red1 ind
R2533:2534 LamSF_reduction <> N' var
R2531:2531 LamSF_reduction <> N var
R2660:2663 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2664:2673 LamSF_reduction <> lamSF_red1 ind
R2684:2686 LamSF_Terms <> Abs constr
R2688:2689 LamSF_reduction <> M' var
R2676:2678 LamSF_Terms <> Abs constr
R2680:2680 LamSF_reduction <> M var
R2645:2654 LamSF_reduction <> lamSF_red1 ind
R2658:2659 LamSF_reduction <> M' var
R2656:2656 LamSF_reduction <> M var
R2726:2730 LamSF_Terms <> lamSF ind
R2755:2764 LamSF_reduction <> lamSF_red1 ind
R2783:2787 LamSF_Terms <> subst def
R2791:2791 LamSF_reduction <> M var
R2789:2789 LamSF_reduction <> N var
R2767:2769 LamSF_Terms <> App constr
R2779:2779 LamSF_reduction <> N var
R2772:2774 LamSF_Terms <> Abs constr
R2776:2776 LamSF_reduction <> M var
R2827:2831 LamSF_Terms <> lamSF ind
R2848:2857 LamSF_reduction <> lamSF_red1 ind
R2932:2934 LamSF_Terms <> App constr
R2947:2949 LamSF_Terms <> App constr
R2953:2953 LamSF_reduction <> P var
R2951:2951 LamSF_reduction <> N var
R2937:2939 LamSF_Terms <> App constr
R2943:2943 LamSF_reduction <> P var
R2941:2941 LamSF_reduction <> M var
R2880:2882 LamSF_Terms <> App constr
R2909:2909 LamSF_reduction <> P var
R2885:2887 LamSF_Terms <> App constr
R2906:2906 LamSF_reduction <> N var
R2890:2892 LamSF_Terms <> App constr
R2903:2903 LamSF_reduction <> M var
R2895:2896 LamSF_Terms <> Op constr
R2898:2900 LamSF_Terms <> Sop constr
R3009:3018 LamSF_reduction <> lamSF_red1 ind
R3058:3058 LamSF_reduction <> M var
R3021:3023 LamSF_Terms <> App constr
R3055:3055 LamSF_reduction <> N var
R3026:3028 LamSF_Terms <> App constr
R3052:3052 LamSF_reduction <> M var
R3031:3033 LamSF_Terms <> App constr
R3045:3046 LamSF_Terms <> Op constr
R3048:3048 LamSF_reduction <> o var
R3036:3037 LamSF_Terms <> Op constr
R3039:3041 LamSF_Terms <> Fop constr
R3103:3107 LamSF_Terms <> lamSF ind
R3121:3138 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3139:3148 LamSF_reduction <> lamSF_red1 ind
R3202:3204 LamSF_Terms <> App constr
R3234:3248 SF_reduction <> right_component def
R3250:3250 LamSF_reduction <> P var
R3207:3209 LamSF_Terms <> App constr
R3214:3227 SF_reduction <> left_component def
R3229:3229 LamSF_reduction <> P var
R3211:3211 LamSF_reduction <> N var
R3151:3153 LamSF_Terms <> App constr
R3176:3176 LamSF_reduction <> N var
R3156:3158 LamSF_Terms <> App constr
R3173:3173 LamSF_reduction <> M var
R3161:3163 LamSF_Terms <> App constr
R3170:3170 LamSF_reduction <> P var
R3165:3168 SF_reduction <> f_op def
R3111:3118 SF_reduction <> compound ind
R3120:3120 LamSF_reduction <> P var
def 3268:3276 <> lamSF_red
R3281:3290 LamSF_Tactics <> multi_step ind
R3292:3301 LamSF_reduction <> lamSF_red1 ind
prf 3438:3457 <> reflective_lamSF_red
R3460:3469 LamSF_Tactics <> reflective def
R3471:3479 LamSF_reduction <> lamSF_red def
def 3562:3574 <> preserves_apl
R3583:3589 LamSF_Tactics <> termred def
R3619:3622 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3623:3625 LamSF_reduction <> red var
R3638:3640 LamSF_Terms <> App constr
R3645:3645 LamSF_reduction <> N var
R3642:3643 LamSF_reduction <> M' var
R3628:3630 LamSF_Terms <> App constr
R3634:3634 LamSF_reduction <> N var
R3632:3632 LamSF_reduction <> M var
R3611:3613 LamSF_reduction <> red var
R3617:3618 LamSF_reduction <> M' var
R3615:3615 LamSF_reduction <> M var
def 3661:3673 <> preserves_apr
R3682:3688 LamSF_Tactics <> termred def
R3718:3721 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3722:3724 LamSF_reduction <> red var
R3737:3739 LamSF_Terms <> App constr
R3743:3744 LamSF_reduction <> N' var
R3741:3741 LamSF_reduction <> M var
R3727:3729 LamSF_Terms <> App constr
R3733:3733 LamSF_reduction <> N var
R3731:3731 LamSF_reduction <> M var
R3710:3712 LamSF_reduction <> red var
R3716:3717 LamSF_reduction <> N' var
R3714:3714 LamSF_reduction <> N var
prf 3755:3778 <> preserves_apl_multi_step
R3795:3801 LamSF_Tactics <> termred def
R3822:3825 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3826:3838 LamSF_reduction <> preserves_apl def
R3841:3850 LamSF_Tactics <> multi_step ind
R3852:3854 LamSF_reduction <> red var
R3805:3817 LamSF_reduction <> preserves_apl def
R3819:3821 LamSF_reduction <> red var
R3916:3918 LamSF_Terms <> App constr
R3901:3908 LamSF_Tactics <> succ_red constr
R3916:3918 LamSF_Terms <> App constr
R3901:3908 LamSF_Tactics <> succ_red constr
prf 3946:3969 <> preserves_apr_multi_step
R3986:3992 LamSF_Tactics <> termred def
R4013:4016 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4017:4029 LamSF_reduction <> preserves_apr def
R4032:4041 LamSF_Tactics <> multi_step ind
R4043:4045 LamSF_reduction <> red var
R3996:4008 LamSF_reduction <> preserves_apr def
R4010:4012 LamSF_reduction <> red var
R4107:4109 LamSF_Terms <> App constr
R4092:4099 LamSF_Tactics <> succ_red constr
R4107:4109 LamSF_Terms <> App constr
R4092:4099 LamSF_Tactics <> succ_red constr
prf 4137:4159 <> preserves_apl_lamSF_red
R4162:4174 LamSF_reduction <> preserves_apl def
R4176:4184 LamSF_reduction <> lamSF_red def
R4203:4226 LamSF_reduction <> preserves_apl_multi_step thm
prf 4296:4318 <> preserves_apr_lamSF_red
R4321:4333 LamSF_reduction <> preserves_apr def
R4335:4343 LamSF_reduction <> lamSF_red def
R4362:4385 LamSF_reduction <> preserves_apr_multi_step thm
prf 4457:4479 <> preserves_app_lamSF_red
R4482:4494 LamSF_Tactics <> preserves_app def
R4496:4504 LamSF_reduction <> lamSF_red def
R4560:4562 LamSF_Terms <> App constr
R4539:4552 LamSF_Tactics <> transitive_red thm
R4560:4562 LamSF_Terms <> App constr
R4539:4552 LamSF_Tactics <> transitive_red thm
R4591:4613 LamSF_reduction <> preserves_apl_lamSF_red thm
R4625:4647 LamSF_reduction <> preserves_apr_lamSF_red thm
prf 4702:4724 <> preserves_abs_lamSF_red
R4727:4739 LamSF_Tactics <> preserves_abs def
R4741:4749 LamSF_reduction <> lamSF_red def
R4784:4807 LamSF_Tactics <> preserves_abs_multi_step thm
prf 4876:4904 <> lift_rec_preserves_lamSF_red1
R4907:4924 LamSF_Tactics <> lift_rec_preserves def
R4926:4935 LamSF_reduction <> lamSF_red1 ind
R5006:5010 LamSF_Terms <> subst def
R5030:5030 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5030:5030 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5053:5070 LamSF_Substitution_term <> lift_rec_subst_rec thm
R5053:5070 LamSF_Substitution_term <> lift_rec_subst_rec thm
R5053:5070 LamSF_Substitution_term <> lift_rec_subst_rec thm
R5093:5106 LamSF_reduction <> beta_lamSF_red constr
R5127:5157 SF_reduction <> lift_rec_preserves_components_l thm
R5127:5157 SF_reduction <> lift_rec_preserves_components_l thm
R5127:5157 SF_reduction <> lift_rec_preserves_components_l thm
R5169:5199 SF_reduction <> lift_rec_preserves_components_r thm
R5169:5199 SF_reduction <> lift_rec_preserves_components_r thm
R5169:5199 SF_reduction <> lift_rec_preserves_components_r thm
prf 5268:5295 <> lift_rec_preserves_lamSF_red
R5298:5315 LamSF_Tactics <> lift_rec_preserves def
R5317:5325 LamSF_reduction <> lamSF_red def
R5344:5372 LamSF_Tactics <> lift_rec_preserves_multi_step thm
prf 5388:5418 <> subst_rec_preserves_r_lamSF_red
R5421:5441 LamSF_Tactics <> subst_rec_preserves_r def
R5443:5451 LamSF_reduction <> lamSF_red def
R5508:5517 LamSF_Terms <> insert_Ref def
R5525:5531 Test <> compare def
R5525:5531 Test <> compare def
R5577:5580 LamSF_Terms <> lift def
R5591:5618 LamSF_reduction <> lift_rec_preserves_lamSF_red thm
prf 5635:5666 <> lamSF_red1_preserves_star_active
R5691:5694 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5719:5723 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5724:5733 LamSF_reduction <> lamSF_red1 ind
R5745:5748 SF_reduction <> star def
R5750:5750 LamSF_reduction <> N var
R5736:5739 SF_reduction <> star def
R5741:5741 LamSF_reduction <> M var
R5705:5714 LamSF_reduction <> lamSF_red1 ind
R5718:5718 LamSF_reduction <> N var
R5716:5716 LamSF_reduction <> M var
R5687:5689 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5679:5684 LamSF_Tactics <> status def
R5686:5686 LamSF_reduction <> M var
R5845:5857 LamSF_reduction <> abs_lamSF_red constr
R5951:5953 Coq.Init.Logic <> :type_scope:x_'='_x not
R5943:5948 LamSF_Tactics <> status def
R5951:5953 Coq.Init.Logic <> :type_scope:x_'='_x not
R5943:5948 LamSF_Tactics <> status def
R5968:5986 SF_reduction <> compound_not_active thm
prf 6011:6044 <> lamSF_red1_preserves_star_compound
R6067:6070 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6095:6099 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6100:6109 LamSF_reduction <> lamSF_red1 ind
R6121:6124 SF_reduction <> star def
R6126:6126 LamSF_reduction <> N var
R6112:6115 SF_reduction <> star def
R6117:6117 LamSF_reduction <> M var
R6081:6090 LamSF_reduction <> lamSF_red1 ind
R6094:6094 LamSF_reduction <> N var
R6092:6092 LamSF_reduction <> M var
R6057:6064 SF_reduction <> compound ind
R6066:6066 LamSF_reduction <> M var
R6241:6253 LamSF_reduction <> abs_lamSF_red constr
R6307:6338 LamSF_reduction <> lamSF_red1_preserves_star_active thm
prf 6609:6635 <> preserves_status_lamSF_red1
R6662:6665 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6690:6693 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6702:6704 Coq.Init.Logic <> :type_scope:x_'='_x not
R6694:6699 LamSF_Tactics <> status def
R6701:6701 LamSF_reduction <> M var
R6705:6710 LamSF_Tactics <> status def
R6712:6712 LamSF_reduction <> N var
R6676:6685 LamSF_reduction <> lamSF_red1 ind
R6689:6689 LamSF_reduction <> N var
R6687:6687 LamSF_reduction <> M var
R6658:6660 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6650:6655 LamSF_Tactics <> status def
R6657:6657 LamSF_reduction <> M var
R6749:6752 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6764:6767 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6792:6795 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6804:6806 Coq.Init.Logic <> :type_scope:x_'='_x not
R6796:6801 LamSF_Tactics <> status def
R6803:6803 LamSF_reduction <> M var
R6807:6812 LamSF_Tactics <> status def
R6814:6814 LamSF_reduction <> N var
R6778:6787 LamSF_reduction <> lamSF_red1 ind
R6791:6791 LamSF_reduction <> N var
R6789:6789 LamSF_reduction <> M var
R6761:6762 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6753:6758 LamSF_Tactics <> status def
R6760:6760 LamSF_reduction <> M var
R6740:6742 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6739:6739 LamSF_reduction <> p var
R6743:6746 LamSF_Tactics <> rank def
R6748:6748 LamSF_reduction <> M var
R6749:6752 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6764:6767 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6792:6795 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6804:6806 Coq.Init.Logic <> :type_scope:x_'='_x not
R6796:6801 LamSF_Tactics <> status def
R6803:6803 LamSF_reduction <> M var
R6807:6812 LamSF_Tactics <> status def
R6814:6814 LamSF_reduction <> N var
R6778:6787 LamSF_reduction <> lamSF_red1 ind
R6791:6791 LamSF_reduction <> N var
R6789:6789 LamSF_reduction <> M var
R6761:6762 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6753:6758 LamSF_Tactics <> status def
R6760:6760 LamSF_reduction <> M var
R6740:6742 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R6739:6739 LamSF_reduction <> p var
R6743:6746 LamSF_Tactics <> rank def
R6748:6748 LamSF_reduction <> M var
R6880:6881 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6874:6877 LamSF_Tactics <> rank def
R6880:6881 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6874:6877 LamSF_Tactics <> rank def
R6896:6908 LamSF_Tactics <> rank_positive thm
R7043:7045 Coq.Init.Logic <> :type_scope:x_'='_x not
R7035:7040 LamSF_Tactics <> status def
R7046:7051 LamSF_Tactics <> status def
R7043:7045 Coq.Init.Logic <> :type_scope:x_'='_x not
R7035:7040 LamSF_Tactics <> status def
R7046:7051 LamSF_Tactics <> status def
R7845:7847 Coq.Init.Logic <> :type_scope:x_'='_x not
R7836:7841 LamSF_Tactics <> status def
R7845:7847 Coq.Init.Logic <> :type_scope:x_'='_x not
R7836:7841 LamSF_Tactics <> status def
R7862:7880 SF_reduction <> compound_not_active thm
R7975:7981 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7993:7994 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7997:7999 Coq.Init.Logic <> :type_scope:x_'='_x not
R8000:8002 LamSF_Terms <> App constr
R8025:8026 LamSF_reduction <> m0 var
R8005:8007 LamSF_Terms <> App constr
R8021:8022 LamSF_reduction <> m2 var
R8010:8012 LamSF_Terms <> App constr
R8017:8018 LamSF_reduction <> m4 var
R8014:8015 LamSF_reduction <> m3 var
R7975:7981 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7993:7994 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7997:7999 Coq.Init.Logic <> :type_scope:x_'='_x not
R8000:8002 LamSF_Terms <> App constr
R8025:8026 LamSF_reduction <> m0 var
R8005:8007 LamSF_Terms <> App constr
R8021:8022 LamSF_reduction <> m2 var
R8010:8012 LamSF_Terms <> App constr
R8017:8018 LamSF_reduction <> m4 var
R8014:8015 LamSF_reduction <> m3 var
R8354:8356 Coq.Init.Logic <> :type_scope:x_'='_x not
R8346:8351 LamSF_Tactics <> status def
R8354:8356 Coq.Init.Logic <> :type_scope:x_'='_x not
R8346:8351 LamSF_Tactics <> status def
R8371:8389 SF_reduction <> compound_not_active thm
R8515:8517 Coq.Init.Logic <> :type_scope:x_'='_x not
R8507:8512 LamSF_Tactics <> status def
R8515:8517 Coq.Init.Logic <> :type_scope:x_'='_x not
R8507:8512 LamSF_Tactics <> status def
R8532:8550 SF_reduction <> compound_not_active thm
R8678:8680 Coq.Init.Logic <> :type_scope:x_'='_x not
R8669:8674 LamSF_Tactics <> status def
R8678:8680 Coq.Init.Logic <> :type_scope:x_'='_x not
R8669:8674 LamSF_Tactics <> status def
R8695:8713 SF_reduction <> compound_not_active thm
R8839:8841 Coq.Init.Logic <> :type_scope:x_'='_x not
R8794:8799 LamSF_Tactics <> status def
R8802:8804 LamSF_Terms <> App constr
R8807:8809 LamSF_Terms <> App constr
R8812:8814 LamSF_Terms <> App constr
R8817:8819 LamSF_Terms <> App constr
R8842:8847 LamSF_Tactics <> status def
R8851:8853 LamSF_Terms <> App constr
R8856:8858 LamSF_Terms <> App constr
R8861:8863 LamSF_Terms <> App constr
R8839:8841 Coq.Init.Logic <> :type_scope:x_'='_x not
R8794:8799 LamSF_Tactics <> status def
R8802:8804 LamSF_Terms <> App constr
R8807:8809 LamSF_Terms <> App constr
R8812:8814 LamSF_Terms <> App constr
R8817:8819 LamSF_Terms <> App constr
R8842:8847 LamSF_Tactics <> status def
R8851:8853 LamSF_Terms <> App constr
R8856:8858 LamSF_Terms <> App constr
R8861:8863 LamSF_Terms <> App constr
R8979:8981 Coq.Init.Logic <> :type_scope:x_'='_x not
R8935:8940 LamSF_Tactics <> status def
R8943:8945 LamSF_Terms <> App constr
R8948:8950 LamSF_Terms <> App constr
R8953:8955 LamSF_Terms <> App constr
R8958:8960 LamSF_Terms <> App constr
R8982:8987 LamSF_Tactics <> status def
R8990:8992 LamSF_Terms <> App constr
R8995:8997 LamSF_Terms <> App constr
R9000:9002 LamSF_Terms <> App constr
R8979:8981 Coq.Init.Logic <> :type_scope:x_'='_x not
R8935:8940 LamSF_Tactics <> status def
R8943:8945 LamSF_Terms <> App constr
R8948:8950 LamSF_Terms <> App constr
R8953:8955 LamSF_Terms <> App constr
R8958:8960 LamSF_Terms <> App constr
R8982:8987 LamSF_Tactics <> status def
R8990:8992 LamSF_Terms <> App constr
R8995:8997 LamSF_Terms <> App constr
R9000:9002 LamSF_Terms <> App constr
prf 9104:9132 <> preserves_compound_lamSF_red1
R9148:9152 LamSF_Terms <> lamSF ind
R9172:9178 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9189:9195 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9206:9212 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9196:9203 SF_reduction <> compound ind
R9205:9205 LamSF_reduction <> N var
R9260:9266 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9213:9221 LamSF_reduction <> lamSF_red def
R9243:9256 SF_reduction <> left_component def
R9258:9258 LamSF_reduction <> N var
R9224:9237 SF_reduction <> left_component def
R9239:9239 LamSF_reduction <> M var
R9267:9275 LamSF_reduction <> lamSF_red def
R9298:9312 SF_reduction <> right_component def
R9314:9314 LamSF_reduction <> N var
R9278:9292 SF_reduction <> right_component def
R9294:9294 LamSF_reduction <> M var
R9179:9186 SF_reduction <> compound ind
R9188:9188 LamSF_reduction <> M var
R9158:9167 LamSF_reduction <> lamSF_red1 ind
R9171:9171 LamSF_reduction <> N var
R9169:9169 LamSF_reduction <> M var
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9398:9407 LamSF_reduction <> lamSF_red1 ind
R9569:9589 SF_reduction <> abs_compound_compound constr
R9650:9663 LamSF_reduction <> appl_lamSF_red constr
R9682:9695 LamSF_reduction <> appr_lamSF_red constr
R9708:9741 LamSF_reduction <> lamSF_red1_preserves_star_compound thm
R9753:9771 SF_reduction <> abs_active_compound constr
R9790:9792 Coq.Init.Logic <> :type_scope:x_'='_x not
R9782:9787 LamSF_Tactics <> status def
R9793:9798 LamSF_Tactics <> status def
R9790:9792 Coq.Init.Logic <> :type_scope:x_'='_x not
R9782:9787 LamSF_Tactics <> status def
R9793:9798 LamSF_Tactics <> status def
R9814:9840 LamSF_reduction <> preserves_status_lamSF_red1 thm
R9883:9914 LamSF_reduction <> lamSF_red1_preserves_star_active thm
R9986:9988 SF_reduction <> bop def
R9986:9988 SF_reduction <> bop def
R10015:10024 LamSF_Tactics <> multi_step ind
R10040:10042 LamSF_Terms <> Ref constr
R10032:10034 LamSF_Terms <> Ref constr
R10026:10029 SF_reduction <> bop1 def
R10015:10024 LamSF_Tactics <> multi_step ind
R10040:10042 LamSF_Terms <> Ref constr
R10032:10034 LamSF_Terms <> Ref constr
R10026:10029 SF_reduction <> bop1 def
R10078:10087 LamSF_Tactics <> multi_step ind
R10099:10102 SF_reduction <> f_op def
R10094:10097 SF_reduction <> f_op def
R10089:10092 SF_reduction <> bop1 def
R10078:10087 LamSF_Tactics <> multi_step ind
R10099:10102 SF_reduction <> f_op def
R10094:10097 SF_reduction <> f_op def
R10089:10092 SF_reduction <> bop1 def
R10135:10144 LamSF_Tactics <> multi_step ind
R10160:10162 LamSF_Terms <> Abs constr
R10152:10154 LamSF_Terms <> Abs constr
R10146:10149 SF_reduction <> bop1 def
R10135:10144 LamSF_Tactics <> multi_step ind
R10160:10162 LamSF_Terms <> Abs constr
R10152:10154 LamSF_Terms <> Abs constr
R10146:10149 SF_reduction <> bop1 def
R10211:10220 LamSF_Tactics <> multi_step ind
R10238:10240 LamSF_Terms <> App constr
R10228:10230 LamSF_Terms <> App constr
R10222:10225 SF_reduction <> bop1 def
R10211:10220 LamSF_Tactics <> multi_step ind
R10238:10240 LamSF_Terms <> App constr
R10228:10230 LamSF_Terms <> App constr
R10222:10225 SF_reduction <> bop1 def
R10291:10300 LamSF_Tactics <> multi_step ind
R10327:10340 SF_reduction <> left_component def
R10308:10321 SF_reduction <> left_component def
R10302:10305 SF_reduction <> bop1 def
R10291:10300 LamSF_Tactics <> multi_step ind
R10327:10340 SF_reduction <> left_component def
R10308:10321 SF_reduction <> left_component def
R10302:10305 SF_reduction <> bop1 def
R10394:10403 LamSF_Tactics <> multi_step ind
R10431:10445 SF_reduction <> right_component def
R10411:10425 SF_reduction <> right_component def
R10405:10408 SF_reduction <> bop1 def
R10394:10403 LamSF_Tactics <> multi_step ind
R10431:10445 SF_reduction <> right_component def
R10411:10425 SF_reduction <> right_component def
R10405:10408 SF_reduction <> bop1 def
R10498:10507 LamSF_Tactics <> multi_step ind
R10532:10539 LamSF_Terms <> lift_rec def
R10515:10522 LamSF_Terms <> lift_rec def
R10509:10512 SF_reduction <> bop1 def
R10498:10507 LamSF_Tactics <> multi_step ind
R10532:10539 LamSF_Terms <> lift_rec def
R10515:10522 LamSF_Terms <> lift_rec def
R10509:10512 SF_reduction <> bop1 def
R10596:10599 SF_reduction <> bop1 def
R10612:10614 LamSF_Terms <> App constr
R10602:10604 LamSF_Terms <> App constr
R10596:10599 SF_reduction <> bop1 def
R10612:10614 LamSF_Terms <> App constr
R10602:10604 LamSF_Terms <> App constr
R10666:10669 SF_reduction <> bop1 def
R10691:10704 SF_reduction <> left_component def
R10672:10685 SF_reduction <> left_component def
R10666:10669 SF_reduction <> bop1 def
R10691:10704 SF_reduction <> left_component def
R10672:10685 SF_reduction <> left_component def
R10759:10762 SF_reduction <> bop1 def
R10785:10799 SF_reduction <> right_component def
R10765:10779 SF_reduction <> right_component def
R10759:10762 SF_reduction <> bop1 def
R10785:10799 SF_reduction <> right_component def
R10765:10779 SF_reduction <> right_component def
R10853:10856 SF_reduction <> bop1 def
R10876:10883 LamSF_Terms <> lift_rec def
R10859:10866 LamSF_Terms <> lift_rec def
R10853:10856 SF_reduction <> bop1 def
R10876:10883 LamSF_Terms <> lift_rec def
R10859:10866 LamSF_Terms <> lift_rec def
R10942:10945 SF_reduction <> bop1 def
R10942:10945 SF_reduction <> bop1 def
R10954:10961 SF_reduction <> compound ind
R10954:10961 SF_reduction <> compound ind
R11005:11008 SF_reduction <> bop1 def
R11011:11024 SF_reduction <> left_component def
R11005:11008 SF_reduction <> bop1 def
R11011:11024 SF_reduction <> left_component def
R11071:11074 SF_reduction <> bop1 def
R11077:11091 SF_reduction <> right_component def
R11071:11074 SF_reduction <> bop1 def
R11077:11091 SF_reduction <> right_component def
R11219:11227 LamSF_reduction <> lamSF_red def
R11219:11227 LamSF_reduction <> lamSF_red def
R11256:11265 LamSF_Tactics <> multi_step ind
R11287:11289 LamSF_Terms <> Ref constr
R11279:11281 LamSF_Terms <> Ref constr
R11267:11276 LamSF_reduction <> lamSF_red1 ind
R11256:11265 LamSF_Tactics <> multi_step ind
R11287:11289 LamSF_Terms <> Ref constr
R11279:11281 LamSF_Terms <> Ref constr
R11267:11276 LamSF_reduction <> lamSF_red1 ind
R11316:11325 LamSF_Tactics <> multi_step ind
R11343:11346 SF_reduction <> f_op def
R11338:11341 SF_reduction <> f_op def
R11327:11336 LamSF_reduction <> lamSF_red1 ind
R11316:11325 LamSF_Tactics <> multi_step ind
R11343:11346 SF_reduction <> f_op def
R11338:11341 SF_reduction <> f_op def
R11327:11336 LamSF_reduction <> lamSF_red1 ind
R11381:11390 LamSF_Tactics <> multi_step ind
R11414:11416 LamSF_Terms <> App constr
R11404:11406 LamSF_Terms <> App constr
R11392:11401 LamSF_reduction <> lamSF_red1 ind
R11381:11390 LamSF_Tactics <> multi_step ind
R11414:11416 LamSF_Terms <> App constr
R11404:11406 LamSF_Terms <> App constr
R11392:11401 LamSF_reduction <> lamSF_red1 ind
R11475:11484 LamSF_Tactics <> multi_step ind
R11506:11508 LamSF_Terms <> Abs constr
R11498:11500 LamSF_Terms <> Abs constr
R11486:11495 LamSF_reduction <> lamSF_red1 ind
R11475:11484 LamSF_Tactics <> multi_step ind
R11506:11508 LamSF_Terms <> Abs constr
R11498:11500 LamSF_Terms <> Abs constr
R11486:11495 LamSF_reduction <> lamSF_red1 ind
R11564:11573 LamSF_reduction <> lamSF_red1 ind
R11584:11586 LamSF_Terms <> Abs constr
R11576:11578 LamSF_Terms <> Abs constr
R11564:11573 LamSF_reduction <> lamSF_red1 ind
R11584:11586 LamSF_Terms <> Abs constr
R11576:11578 LamSF_Terms <> Abs constr
R11633:11642 LamSF_reduction <> lamSF_red1 ind
R11662:11669 LamSF_Terms <> lift_rec def
R11645:11652 LamSF_Terms <> lift_rec def
R11633:11642 LamSF_reduction <> lamSF_red1 ind
R11662:11669 LamSF_Terms <> lift_rec def
R11645:11652 LamSF_Terms <> lift_rec def
R11800:11809 LamSF_Tactics <> sequential ind
R11800:11809 LamSF_Tactics <> sequential ind
R11830:11836 LamSF_Tactics <> seq_red constr
R11893:11902 LamSF_Tactics <> sequential ind
R11893:11902 LamSF_Tactics <> sequential ind
R11923:11929 LamSF_Tactics <> seq_red constr
def 11961:11971 <> implies_red
R11985:11991 LamSF_Tactics <> termred def
R12017:12020 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12021:12024 LamSF_reduction <> red2 var
R12028:12028 LamSF_reduction <> N var
R12026:12026 LamSF_reduction <> M var
R12009:12012 LamSF_reduction <> red1 var
R12016:12016 LamSF_reduction <> N var
R12014:12014 LamSF_reduction <> M var
prf 12039:12060 <> implies_red_multi_step
R12116:12168 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12169:12179 LamSF_reduction <> implies_red def
R12200:12209 LamSF_Tactics <> multi_step ind
R12211:12214 LamSF_reduction <> red2 var
R12182:12191 LamSF_Tactics <> multi_step ind
R12193:12196 LamSF_reduction <> red1 var
R12081:12091 LamSF_reduction <> implies_red def
R12100:12109 LamSF_Tactics <> multi_step ind
R12111:12114 LamSF_reduction <> red2 var
R12093:12096 LamSF_reduction <> red1 var
R12289:12302 LamSF_Tactics <> transitive_red thm
R12289:12302 LamSF_Tactics <> transitive_red thm
prf 12331:12345 <> implies_red_seq
R12411:12419 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12454:12460 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12461:12471 LamSF_reduction <> implies_red def
R12497:12506 LamSF_Tactics <> multi_step ind
R12508:12511 LamSF_reduction <> red3 var
R12474:12483 LamSF_Tactics <> sequential ind
R12490:12493 LamSF_reduction <> red2 var
R12485:12488 LamSF_reduction <> red1 var
R12420:12430 LamSF_reduction <> implies_red def
R12438:12447 LamSF_Tactics <> multi_step ind
R12449:12452 LamSF_reduction <> red3 var
R12432:12435 LamSF_reduction <> red2 var
R12376:12386 LamSF_reduction <> implies_red def
R12395:12404 LamSF_Tactics <> multi_step ind
R12406:12409 LamSF_reduction <> red3 var
R12388:12391 LamSF_reduction <> red1 var
R12560:12573 LamSF_Tactics <> transitive_red thm
R12560:12573 LamSF_Tactics <> transitive_red thm
prf 12605:12622 <> lamSF_red1_to_bop1
R12626:12636 LamSF_reduction <> implies_red def
R12649:12652 SF_reduction <> bop1 def
R12638:12647 LamSF_reduction <> lamSF_red1 ind
R12685:12692 LamSF_Tactics <> succ_red constr
R12987:12989 LamSF_Terms <> Abs constr
R12973:12979 LamSF_Tactics <> seq_red constr
R12987:12989 LamSF_Terms <> Abs constr
R12973:12979 LamSF_Tactics <> seq_red constr
R12685:12692 LamSF_Tactics <> succ_red constr
prf 13021:13036 <> lamSF_red_to_bop
R13039:13049 LamSF_reduction <> implies_red def
R13061:13063 SF_reduction <> bop def
R13051:13059 LamSF_reduction <> lamSF_red def
R13083:13104 LamSF_reduction <> implies_red_multi_step thm
R13142:13159 LamSF_reduction <> lamSF_red1_to_bop1 thm
prf 13178:13200 <> to_lamSF_red_multi_step
R13240:13243 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13244:13254 LamSF_reduction <> implies_red def
R13273:13281 LamSF_reduction <> lamSF_red def
R13257:13266 LamSF_Tactics <> multi_step ind
R13268:13270 LamSF_reduction <> red var
R13215:13225 LamSF_reduction <> implies_red def
R13231:13239 LamSF_reduction <> lamSF_red def
R13227:13229 LamSF_reduction <> red var
R13367:13375 LamSF_reduction <> lamSF_red def
R13367:13375 LamSF_reduction <> lamSF_red def
R13403:13416 LamSF_Tactics <> transitive_red thm
R13403:13416 LamSF_Tactics <> transitive_red thm
prf 13460:13475 <> to_lamSF_red_seq
R13522:13525 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13552:13556 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13557:13567 LamSF_reduction <> implies_red def
R13593:13601 LamSF_reduction <> lamSF_red def
R13571:13580 LamSF_Tactics <> sequential ind
R13587:13590 LamSF_reduction <> red2 var
R13582:13585 LamSF_reduction <> red1 var
R13526:13536 LamSF_reduction <> implies_red def
R13543:13551 LamSF_reduction <> lamSF_red def
R13538:13541 LamSF_reduction <> red2 var
R13496:13506 LamSF_reduction <> implies_red def
R13513:13521 LamSF_reduction <> lamSF_red def
R13508:13511 LamSF_reduction <> red1 var
R13656:13669 LamSF_Tactics <> transitive_red thm
R13656:13669 LamSF_Tactics <> transitive_red thm
R13738:13745 LamSF_Tactics <> succ_red constr
R13802:13811 LamSF_reduction <> lamSF_red1 ind
R13816:13818 LamSF_Terms <> App constr
R13821:13823 LamSF_Terms <> App constr
R13802:13811 LamSF_reduction <> lamSF_red1 ind
R13816:13818 LamSF_Terms <> App constr
R13821:13823 LamSF_Terms <> App constr
R13854:13867 SF_reduction <> left_component def
R13870:13872 LamSF_Terms <> App constr
R13907:13921 SF_reduction <> right_component def
R13924:13926 LamSF_Terms <> App constr
def 13966:13987 <> preserves_components_l
R13995:14001 LamSF_Tactics <> termred def
R14028:14031 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14049:14052 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14063:14067 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R14053:14060 SF_reduction <> compound ind
R14062:14062 LamSF_reduction <> N var
R14068:14077 LamSF_Tactics <> multi_step ind
R14103:14116 SF_reduction <> left_component def
R14118:14118 LamSF_reduction <> N var
R14084:14097 SF_reduction <> left_component def
R14099:14099 LamSF_reduction <> M var
R14079:14081 LamSF_reduction <> red var
R14042:14044 LamSF_reduction <> red var
R14048:14048 LamSF_reduction <> N var
R14046:14046 LamSF_reduction <> M var
R14018:14025 SF_reduction <> compound ind
R14027:14027 LamSF_reduction <> M var
prf 14129:14161 <> preserves_components_l_multi_step
R14204:14208 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14229:14232 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14261:14264 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14275:14279 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R14265:14272 SF_reduction <> compound ind
R14274:14274 LamSF_reduction <> N var
R14280:14289 LamSF_Tactics <> multi_step ind
R14315:14328 SF_reduction <> left_component def
R14330:14330 LamSF_reduction <> N var
R14296:14309 SF_reduction <> left_component def
R14311:14311 LamSF_reduction <> M var
R14291:14293 LamSF_reduction <> red var
R14243:14252 LamSF_Tactics <> multi_step ind
R14260:14260 LamSF_reduction <> N var
R14258:14258 LamSF_reduction <> M var
R14254:14256 LamSF_reduction <> red var
R14219:14226 SF_reduction <> compound ind
R14228:14228 LamSF_reduction <> M var
R14178:14199 LamSF_reduction <> preserves_components_l def
R14201:14203 LamSF_reduction <> red var
R14441:14454 SF_reduction <> left_component def
R14420:14433 LamSF_Tactics <> transitive_red thm
R14441:14454 SF_reduction <> left_component def
R14420:14433 LamSF_Tactics <> transitive_red thm
def 14529:14550 <> preserves_components_r
R14558:14564 LamSF_Tactics <> termred def
R14591:14594 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14612:14615 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14626:14630 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R14616:14623 SF_reduction <> compound ind
R14625:14625 LamSF_reduction <> N var
R14631:14640 LamSF_Tactics <> multi_step ind
R14667:14681 SF_reduction <> right_component def
R14683:14683 LamSF_reduction <> N var
R14647:14661 SF_reduction <> right_component def
R14663:14663 LamSF_reduction <> M var
R14642:14644 LamSF_reduction <> red var
R14605:14607 LamSF_reduction <> red var
R14611:14611 LamSF_reduction <> N var
R14609:14609 LamSF_reduction <> M var
R14581:14588 SF_reduction <> compound ind
R14590:14590 LamSF_reduction <> M var
prf 14695:14727 <> preserves_components_r_multi_step
R14770:14774 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14795:14798 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14827:14830 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14841:14845 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R14831:14838 SF_reduction <> compound ind
R14840:14840 LamSF_reduction <> N var
R14846:14855 LamSF_Tactics <> multi_step ind
R14882:14896 SF_reduction <> right_component def
R14898:14898 LamSF_reduction <> N var
R14862:14876 SF_reduction <> right_component def
R14878:14878 LamSF_reduction <> M var
R14857:14859 LamSF_reduction <> red var
R14809:14818 LamSF_Tactics <> multi_step ind
R14826:14826 LamSF_reduction <> N var
R14824:14824 LamSF_reduction <> M var
R14820:14822 LamSF_reduction <> red var
R14785:14792 SF_reduction <> compound ind
R14794:14794 LamSF_reduction <> M var
R14744:14765 LamSF_reduction <> preserves_components_r def
R14767:14769 LamSF_reduction <> red var
R15009:15023 SF_reduction <> right_component def
R14988:15001 LamSF_Tactics <> transitive_red thm
R15009:15023 SF_reduction <> right_component def
R14988:15001 LamSF_Tactics <> transitive_red thm
prf 15091:15123 <> preserves_components_l_lamSF_red1
R15128:15149 LamSF_reduction <> preserves_components_l def
R15151:15160 LamSF_reduction <> lamSF_red1 ind
R15208:15215 SF_reduction <> compound ind
R15208:15215 SF_reduction <> compound ind
R15208:15215 SF_reduction <> compound ind
R15208:15215 SF_reduction <> compound ind
R15208:15215 SF_reduction <> compound ind
R15208:15215 SF_reduction <> compound ind
R15208:15215 SF_reduction <> compound ind
R15348:15368 SF_reduction <> abs_compound_compound constr
R15380:15408 LamSF_reduction <> preserves_compound_lamSF_red1 thm
R15429:15447 SF_reduction <> abs_active_compound constr
R15467:15469 Coq.Init.Logic <> :type_scope:x_'='_x not
R15458:15463 LamSF_Tactics <> status def
R15470:15475 LamSF_Tactics <> status def
R15467:15469 Coq.Init.Logic <> :type_scope:x_'='_x not
R15458:15463 LamSF_Tactics <> status def
R15470:15475 LamSF_Tactics <> status def
R15490:15516 LamSF_reduction <> preserves_status_lamSF_red1 thm
prf 15817:15849 <> preserves_components_r_lamSF_red1
R15854:15875 LamSF_reduction <> preserves_components_r def
R15877:15886 LamSF_reduction <> lamSF_red1 ind
R15934:15941 SF_reduction <> compound ind
R15934:15941 SF_reduction <> compound ind
R15934:15941 SF_reduction <> compound ind
R15934:15941 SF_reduction <> compound ind
R15934:15941 SF_reduction <> compound ind
R15934:15941 SF_reduction <> compound ind
R15934:15941 SF_reduction <> compound ind
R16073:16093 SF_reduction <> abs_compound_compound constr
R16105:16133 LamSF_reduction <> preserves_compound_lamSF_red1 thm
R16145:16163 SF_reduction <> abs_active_compound constr
R16183:16185 Coq.Init.Logic <> :type_scope:x_'='_x not
R16174:16179 LamSF_Tactics <> status def
R16186:16191 LamSF_Tactics <> status def
R16183:16185 Coq.Init.Logic <> :type_scope:x_'='_x not
R16174:16179 LamSF_Tactics <> status def
R16186:16191 LamSF_Tactics <> status def
R16206:16232 LamSF_reduction <> preserves_status_lamSF_red1 thm
R16280:16287 SF_reduction <> compound ind
R16280:16287 SF_reduction <> compound ind
R16280:16287 SF_reduction <> compound ind
R16280:16287 SF_reduction <> compound ind
R16280:16287 SF_reduction <> compound ind
R16280:16287 SF_reduction <> compound ind
R16372:16385 LamSF_reduction <> appl_lamSF_red constr
R16405:16418 LamSF_reduction <> appr_lamSF_red constr
R16431:16464 LamSF_reduction <> lamSF_red1_preserves_star_compound thm
R16476:16507 LamSF_reduction <> lamSF_red1_preserves_star_active thm
prf 16532:16550 <> opred1_to_lamSF_red
R16553:16563 LamSF_reduction <> implies_red def
R16572:16580 LamSF_reduction <> lamSF_red def
R16565:16570 SF_reduction <> opred1 ind
R16668:16670 LamSF_Terms <> App constr
R16683:16685 LamSF_Terms <> App constr
R16673:16675 LamSF_Terms <> App constr
R16653:16660 LamSF_Tactics <> succ_red constr
R16668:16670 LamSF_Terms <> App constr
R16683:16685 LamSF_Terms <> App constr
R16673:16675 LamSF_Terms <> App constr
R16653:16660 LamSF_Tactics <> succ_red constr
R16702:16712 LamSF_reduction <> s_lamSF_red constr
R16724:16746 LamSF_reduction <> preserves_app_lamSF_red thm
R16756:16763 LamSF_Tactics <> succ_red constr
R16756:16763 LamSF_Tactics <> succ_red constr
R16782:16795 LamSF_reduction <> f_op_lamSF_red constr
R16832:16834 LamSF_Terms <> App constr
R16864:16878 SF_reduction <> right_component def
R16837:16839 LamSF_Terms <> App constr
R16844:16857 SF_reduction <> left_component def
R16816:16823 LamSF_Tactics <> succ_red constr
R16832:16834 LamSF_Terms <> App constr
R16864:16878 SF_reduction <> right_component def
R16837:16839 LamSF_Terms <> App constr
R16844:16857 SF_reduction <> left_component def
R16816:16823 LamSF_Tactics <> succ_red constr
R16915:16923 LamSF_reduction <> lamSF_red def
R16915:16923 LamSF_reduction <> lamSF_red def
R16935:16967 LamSF_reduction <> preserves_components_l_multi_step thm
R16979:17011 LamSF_reduction <> preserves_components_l_lamSF_red1 thm
R17023:17055 LamSF_reduction <> preserves_components_r_multi_step thm
R17067:17099 LamSF_reduction <> preserves_components_r_lamSF_red1 thm
prf 17151:17171 <> par_red1_to_lamSF_red
R17174:17184 LamSF_reduction <> implies_red def
R17195:17203 LamSF_reduction <> lamSF_red def
R17186:17193 Beta_Reduction <> par_red1 ind
R17289:17291 LamSF_Terms <> App constr
R17294:17296 LamSF_Terms <> Abs constr
R17268:17281 LamSF_Tactics <> transitive_red thm
R17289:17291 LamSF_Terms <> App constr
R17294:17296 LamSF_Terms <> Abs constr
R17268:17281 LamSF_Tactics <> transitive_red thm
prf 17382:17398 <> bop1_to_lamSF_red
R17401:17411 LamSF_reduction <> implies_red def
R17418:17426 LamSF_reduction <> lamSF_red def
R17413:17416 SF_reduction <> bop1 def
R17446:17460 LamSF_reduction <> implies_red_seq thm
R17472:17493 LamSF_reduction <> implies_red_multi_step thm
prf 17510:17525 <> bop_to_lamSF_red
R17528:17538 LamSF_reduction <> implies_red def
R17544:17552 LamSF_reduction <> lamSF_red def
R17540:17542 SF_reduction <> bop def
R17572:17593 LamSF_reduction <> implies_red_multi_step thm
R17604:17620 LamSF_reduction <> bop1_to_lamSF_red thm
prf 17638:17654 <> diamond_lamSF_red
R17657:17663 LamSF_Tactics <> diamond def
R17675:17683 LamSF_reduction <> lamSF_red def
R17665:17673 LamSF_reduction <> lamSF_red def
R17719:17721 SF_reduction <> bop def
R17719:17721 SF_reduction <> bop def
R17739:17754 LamSF_reduction <> lamSF_red_to_bop thm
R17766:17768 SF_reduction <> bop def
R17766:17768 SF_reduction <> bop def
R17786:17801 LamSF_reduction <> lamSF_red_to_bop thm
R17811:17821 SF_reduction <> diamond_bop thm
R17811:17821 SF_reduction <> diamond_bop thm
R17863:17878 LamSF_reduction <> bop_to_lamSF_red thm
R17863:17878 LamSF_reduction <> bop_to_lamSF_red thm
prf 17930:17949 <> confluence_lamSF_red
R17952:17961 LamSF_Confluence <> confluence def
R17969:17977 LamSF_reduction <> lamSF_red def
R17963:17967 LamSF_Terms <> lamSF ind
R18000:18016 LamSF_reduction <> diamond_lamSF_red thm