forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Binding.glob
1990 lines (1990 loc) · 83.6 KB
/
Binding.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 28c5c1613bdadb01f2cc6481b3a5d204
FBinding
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:2131 LamSF_Substitution_term <> <> lib
R2149:2161 LamSF_Tactics <> <> lib
R2179:2192 Beta_Reduction <> <> lib
R2210:2225 LamSF_Confluence <> <> lib
R2243:2254 SF_reduction <> <> lib
R2272:2286 LamSF_reduction <> <> lib
R2304:2315 LamSF_Normal <> <> lib
R2333:2344 LamSF_Closed <> <> lib
R2362:2371 LamSF_Eval <> <> lib
R2389:2393 Equal <> <> lib
R2411:2421 Combinators <> <> lib
R2439:2443 Coq.omega.Omega <> <> lib
R2501:2505 LamSF_Terms <> subst def
R2515:2523 LamSF_Terms <> subst_rec def
R2531:2539 LamSF_Terms <> subst_rec def
R2574:2586 LamSF_Substitution_term <> lift_rec_null thm
def 2603:2610 <> binds_fn
R2615:2617 LamSF_Terms <> Abs constr
R2620:2622 LamSF_Terms <> Abs constr
R2626:2628 LamSF_Terms <> App constr
R2674:2676 LamSF_Terms <> App constr
R2720:2722 LamSF_Terms <> Abs constr
R2725:2727 LamSF_Terms <> Abs constr
R2731:2733 LamSF_Terms <> App constr
R2770:2772 LamSF_Terms <> App constr
R2783:2785 LamSF_Terms <> Ref constr
R2775:2777 LamSF_Terms <> Ref constr
R2736:2738 LamSF_Terms <> App constr
R2762:2765 SF_reduction <> k_op def
R2741:2743 LamSF_Terms <> App constr
R2754:2756 LamSF_Terms <> Ref constr
R2746:2748 LamSF_Terms <> Ref constr
R2679:2681 LamSF_Terms <> App constr
R2703:2705 LamSF_Terms <> App constr
R2712:2715 SF_reduction <> i_op def
R2707:2710 SF_reduction <> k_op def
R2684:2686 LamSF_Terms <> App constr
R2694:2696 LamSF_Terms <> Ref constr
R2688:2691 SF_reduction <> f_op def
R2631:2633 LamSF_Terms <> App constr
R2666:2669 SF_reduction <> k_op def
R2636:2638 LamSF_Terms <> App constr
R2658:2660 LamSF_Terms <> Ref constr
R2641:2643 LamSF_Terms <> App constr
R2651:2654 SF_reduction <> i_op def
R2645:2649 Equal <> equal def
def 2811:2815 <> binds
R2820:2822 LamSF_Terms <> App constr
R2833:2840 Binding <> binds_fn def
R2824:2831 LamSF_Eval <> fixpoint def
prf 2852:2861 <> binds_rank
R2884:2887 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2906:2910 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2911:2919 LamSF_reduction <> lamSF_red def
R2936:2938 LamSF_Terms <> App constr
R2945:2948 SF_reduction <> i_op def
R2940:2943 SF_reduction <> k_op def
R2922:2924 LamSF_Terms <> App constr
R2932:2932 Binding <> M var
R2926:2930 Binding <> binds def
R2897:2899 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R2888:2891 LamSF_Tactics <> rank def
R2893:2896 SF_reduction <> i_op def
R2900:2903 LamSF_Tactics <> rank def
R2905:2905 Binding <> M var
R2875:2881 LamSF_Closed <> program def
R2883:2883 Binding <> M var
R2967:2973 LamSF_Closed <> program def
R3064:3068 Binding <> binds def
R3086:3090 Binding <> binds def
R3086:3090 Binding <> binds def
R3100:3107 Binding <> binds_fn def
R3141:3156 LamSF_Closed <> subst_rec_closed thm
R3158:3162 Equal <> equal def
R3141:3156 LamSF_Closed <> subst_rec_closed thm
R3158:3162 Equal <> equal def
R3141:3156 LamSF_Closed <> subst_rec_closed thm
R3158:3162 Equal <> equal def
R3141:3156 LamSF_Closed <> subst_rec_closed thm
R3158:3162 Equal <> equal def
R3141:3156 LamSF_Closed <> subst_rec_closed thm
R3158:3162 Equal <> equal def
R3191:3199 LamSF_Terms <> subst_rec def
R3207:3215 LamSF_Terms <> subst_rec def
R3207:3215 LamSF_Terms <> subst_rec def
R3242:3259 LamSF_Substitution_term <> subst_rec_lift_rec thm
R3242:3259 LamSF_Substitution_term <> subst_rec_lift_rec thm
R3242:3259 LamSF_Substitution_term <> subst_rec_lift_rec thm
R3242:3259 LamSF_Substitution_term <> subst_rec_lift_rec thm
R3242:3259 LamSF_Substitution_term <> subst_rec_lift_rec thm
R3309:3318 LamSF_Tactics <> multi_step ind
R3332:3334 LamSF_Terms <> App constr
R3337:3339 LamSF_Terms <> App constr
R3320:3329 LamSF_reduction <> lamSF_red1 ind
R3309:3318 LamSF_Tactics <> multi_step ind
R3332:3334 LamSF_Terms <> App constr
R3337:3339 LamSF_Terms <> App constr
R3320:3329 LamSF_reduction <> lamSF_red1 ind
R3383:3385 LamSF_Terms <> App constr
R3388:3390 LamSF_Terms <> App constr
R3393:3395 LamSF_Terms <> App constr
R3402:3405 SF_reduction <> i_op def
R3397:3400 SF_reduction <> k_op def
R3362:3375 LamSF_Tactics <> transitive_red thm
R3383:3385 LamSF_Terms <> App constr
R3388:3390 LamSF_Terms <> App constr
R3393:3395 LamSF_Terms <> App constr
R3402:3405 SF_reduction <> i_op def
R3397:3400 SF_reduction <> k_op def
R3362:3375 LamSF_Tactics <> transitive_red thm
R3428:3450 LamSF_reduction <> preserves_app_lamSF_red thm
R3462:3484 LamSF_reduction <> preserves_app_lamSF_red thm
R3496:3511 Equal <> unequal_programs thm
R3618:3620 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3612:3615 LamSF_Tactics <> rank def
R3618:3620 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3612:3615 LamSF_Tactics <> rank def
R3635:3647 LamSF_Tactics <> rank_positive thm
R3705:3708 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R3687:3692 LamSF_Tactics <> status def
R3695:3697 LamSF_Terms <> App constr
R3709:3714 LamSF_Closed <> maxvar def
R3717:3719 LamSF_Terms <> App constr
R3705:3708 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R3687:3692 LamSF_Tactics <> status def
R3695:3697 LamSF_Terms <> App constr
R3709:3714 LamSF_Closed <> maxvar def
R3717:3719 LamSF_Terms <> App constr
R3740:3755 LamSF_Closed <> status_lt_maxvar thm
R3783:3787 Binding <> binds def
R3805:3809 Binding <> binds def
R3805:3809 Binding <> binds def
R3819:3826 Binding <> binds_fn def
R3860:3875 LamSF_Closed <> subst_rec_closed thm
R3877:3881 Equal <> equal def
R3860:3875 LamSF_Closed <> subst_rec_closed thm
R3877:3881 Equal <> equal def
R3860:3875 LamSF_Closed <> subst_rec_closed thm
R3877:3881 Equal <> equal def
R3860:3875 LamSF_Closed <> subst_rec_closed thm
R3877:3881 Equal <> equal def
R3860:3875 LamSF_Closed <> subst_rec_closed thm
R3877:3881 Equal <> equal def
R3910:3918 LamSF_Terms <> subst_rec def
R3926:3934 LamSF_Terms <> subst_rec def
R3926:3934 LamSF_Terms <> subst_rec def
R3968:3980 LamSF_Substitution_term <> lift_rec_null thm
R3968:3980 LamSF_Substitution_term <> lift_rec_null thm
R3968:3980 LamSF_Substitution_term <> lift_rec_null thm
R3968:3980 LamSF_Substitution_term <> lift_rec_null thm
R3968:3980 LamSF_Substitution_term <> lift_rec_null thm
R3968:3980 LamSF_Substitution_term <> lift_rec_null thm
R4007:4016 LamSF_Tactics <> multi_step ind
R4030:4032 LamSF_Terms <> App constr
R4035:4037 LamSF_Terms <> App constr
R4018:4027 LamSF_reduction <> lamSF_red1 ind
R4007:4016 LamSF_Tactics <> multi_step ind
R4030:4032 LamSF_Terms <> App constr
R4035:4037 LamSF_Terms <> App constr
R4018:4027 LamSF_reduction <> lamSF_red1 ind
R4081:4083 LamSF_Terms <> App constr
R4086:4088 LamSF_Terms <> App constr
R4091:4093 LamSF_Terms <> App constr
R4100:4103 SF_reduction <> i_op def
R4095:4098 SF_reduction <> k_op def
R4060:4073 LamSF_Tactics <> transitive_red thm
R4081:4083 LamSF_Terms <> App constr
R4086:4088 LamSF_Terms <> App constr
R4091:4093 LamSF_Terms <> App constr
R4100:4103 SF_reduction <> i_op def
R4095:4098 SF_reduction <> k_op def
R4060:4073 LamSF_Tactics <> transitive_red thm
R4126:4148 LamSF_reduction <> preserves_app_lamSF_red thm
R4160:4182 LamSF_reduction <> preserves_app_lamSF_red thm
R4194:4209 Equal <> unequal_programs thm
R4339:4341 LamSF_Terms <> App constr
R4339:4341 LamSF_Terms <> App constr
R4376:4378 LamSF_Terms <> App constr
R4418:4432 SF_reduction <> right_component def
R4435:4437 LamSF_Terms <> App constr
R4381:4383 LamSF_Terms <> App constr
R4388:4401 SF_reduction <> left_component def
R4404:4406 LamSF_Terms <> App constr
R4361:4368 LamSF_Tactics <> succ_red constr
R4376:4378 LamSF_Terms <> App constr
R4418:4432 SF_reduction <> right_component def
R4435:4437 LamSF_Terms <> App constr
R4381:4383 LamSF_Terms <> App constr
R4388:4401 SF_reduction <> left_component def
R4404:4406 LamSF_Terms <> App constr
R4361:4368 LamSF_Tactics <> succ_red constr
R4461:4480 LamSF_reduction <> f_compound_lamSF_red constr
R4514:4529 LamSF_Closed <> subst_rec_closed thm
R4531:4535 Binding <> binds def
R4514:4529 LamSF_Closed <> subst_rec_closed thm
R4531:4535 Binding <> binds def
R4514:4529 LamSF_Closed <> subst_rec_closed thm
R4531:4535 Binding <> binds def
R4514:4529 LamSF_Closed <> subst_rec_closed thm
R4531:4535 Binding <> binds def
R4514:4529 LamSF_Closed <> subst_rec_closed thm
R4531:4535 Binding <> binds def
R4564:4577 SF_reduction <> left_component def
R4580:4594 SF_reduction <> right_component def
R4606:4623 LamSF_Substitution_term <> subst_rec_lift_rec thm
R4606:4623 LamSF_Substitution_term <> subst_rec_lift_rec thm
R4606:4623 LamSF_Substitution_term <> subst_rec_lift_rec thm
R4606:4623 LamSF_Substitution_term <> subst_rec_lift_rec thm
R4606:4623 LamSF_Substitution_term <> subst_rec_lift_rec thm
R4653:4665 LamSF_Substitution_term <> lift_rec_null thm
R4653:4665 LamSF_Substitution_term <> lift_rec_null thm
R4653:4665 LamSF_Substitution_term <> lift_rec_null thm
R4653:4665 LamSF_Substitution_term <> lift_rec_null thm
R4692:4701 LamSF_Tactics <> multi_step ind
R4715:4717 LamSF_Terms <> App constr
R4720:4722 LamSF_Terms <> App constr
R4703:4712 LamSF_reduction <> lamSF_red1 ind
R4692:4701 LamSF_Tactics <> multi_step ind
R4715:4717 LamSF_Terms <> App constr
R4720:4722 LamSF_Terms <> App constr
R4703:4712 LamSF_reduction <> lamSF_red1 ind
R4766:4768 LamSF_Terms <> App constr
R4771:4773 LamSF_Terms <> App constr
R4776:4778 LamSF_Terms <> App constr
R4785:4788 SF_reduction <> i_op def
R4780:4783 SF_reduction <> k_op def
R4745:4758 LamSF_Tactics <> transitive_red thm
R4766:4768 LamSF_Terms <> App constr
R4771:4773 LamSF_Terms <> App constr
R4776:4778 LamSF_Terms <> App constr
R4785:4788 SF_reduction <> i_op def
R4780:4783 SF_reduction <> k_op def
R4745:4758 LamSF_Tactics <> transitive_red thm
R4811:4833 LamSF_reduction <> preserves_app_lamSF_red thm
R4845:4867 LamSF_reduction <> preserves_app_lamSF_red thm
prf 5030:5038 <> binds_abs
R5067:5071 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5072:5080 LamSF_reduction <> lamSF_red def
R5103:5105 LamSF_Terms <> App constr
R5114:5117 SF_reduction <> star def
R5119:5119 Binding <> M var
R5107:5111 Binding <> binds def
R5083:5085 LamSF_Terms <> App constr
R5094:5096 LamSF_Terms <> Abs constr
R5098:5098 Binding <> M var
R5087:5091 Binding <> binds def
R5052:5058 LamSF_Closed <> program def
R5061:5063 LamSF_Terms <> Abs constr
R5065:5065 Binding <> M var
R5139:5145 LamSF_Closed <> program def
R5168:5172 Binding <> binds def
R5188:5192 Binding <> binds def
R5188:5192 Binding <> binds def
R5202:5209 Binding <> binds_fn def
R5242:5257 LamSF_Closed <> subst_rec_closed thm
R5259:5263 Equal <> equal def
R5242:5257 LamSF_Closed <> subst_rec_closed thm
R5259:5263 Equal <> equal def
R5242:5257 LamSF_Closed <> subst_rec_closed thm
R5259:5263 Equal <> equal def
R5242:5257 LamSF_Closed <> subst_rec_closed thm
R5259:5263 Equal <> equal def
R5242:5257 LamSF_Closed <> subst_rec_closed thm
R5259:5263 Equal <> equal def
R5292:5300 LamSF_Terms <> subst_rec def
R5308:5316 LamSF_Terms <> subst_rec def
R5308:5316 LamSF_Terms <> subst_rec def
R5357:5366 LamSF_Tactics <> multi_step ind
R5380:5382 LamSF_Terms <> App constr
R5385:5387 LamSF_Terms <> App constr
R5368:5377 LamSF_reduction <> lamSF_red1 ind
R5357:5366 LamSF_Tactics <> multi_step ind
R5380:5382 LamSF_Terms <> App constr
R5385:5387 LamSF_Terms <> App constr
R5368:5377 LamSF_reduction <> lamSF_red1 ind
R5431:5433 LamSF_Terms <> App constr
R5436:5438 LamSF_Terms <> App constr
R5441:5443 LamSF_Terms <> App constr
R5450:5453 SF_reduction <> i_op def
R5445:5448 SF_reduction <> k_op def
R5410:5423 LamSF_Tactics <> transitive_red thm
R5431:5433 LamSF_Terms <> App constr
R5436:5438 LamSF_Terms <> App constr
R5441:5443 LamSF_Terms <> App constr
R5450:5453 SF_reduction <> i_op def
R5445:5448 SF_reduction <> k_op def
R5410:5423 LamSF_Tactics <> transitive_red thm
R5476:5498 LamSF_reduction <> preserves_app_lamSF_red thm
R5510:5532 LamSF_reduction <> preserves_app_lamSF_red thm
R5543:5555 LamSF_Substitution_term <> lift_rec_null thm
R5543:5555 LamSF_Substitution_term <> lift_rec_null thm
R5543:5555 LamSF_Substitution_term <> lift_rec_null thm
R5567:5582 Equal <> unequal_programs thm
R5649:5651 LamSF_Terms <> App constr
R5649:5651 LamSF_Terms <> App constr
R5686:5688 LamSF_Terms <> App constr
R5724:5738 SF_reduction <> right_component def
R5741:5743 LamSF_Terms <> Abs constr
R5691:5693 LamSF_Terms <> App constr
R5698:5711 SF_reduction <> left_component def
R5714:5716 LamSF_Terms <> Abs constr
R5671:5678 LamSF_Tactics <> succ_red constr
R5686:5688 LamSF_Terms <> App constr
R5724:5738 SF_reduction <> right_component def
R5741:5743 LamSF_Terms <> Abs constr
R5691:5693 LamSF_Terms <> App constr
R5698:5711 SF_reduction <> left_component def
R5714:5716 LamSF_Terms <> Abs constr
R5671:5678 LamSF_Tactics <> succ_red constr
R5764:5783 LamSF_reduction <> f_compound_lamSF_red constr
R5794:5803 LamSF_Closed <> factorable def
R5806:5808 LamSF_Terms <> Abs constr
R5794:5803 LamSF_Closed <> factorable def
R5806:5808 LamSF_Terms <> Abs constr
R5824:5846 LamSF_Closed <> programs_are_factorable thm
R5917:5932 LamSF_Closed <> subst_rec_closed thm
R5934:5938 Binding <> binds def
R5917:5932 LamSF_Closed <> subst_rec_closed thm
R5934:5938 Binding <> binds def
R5917:5932 LamSF_Closed <> subst_rec_closed thm
R5934:5938 Binding <> binds def
R5917:5932 LamSF_Closed <> subst_rec_closed thm
R5934:5938 Binding <> binds def
R5917:5932 LamSF_Closed <> subst_rec_closed thm
R5934:5938 Binding <> binds def
R5967:5980 SF_reduction <> left_component def
R5983:5997 SF_reduction <> right_component def
R6020:6037 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6020:6037 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6020:6037 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6020:6037 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6020:6037 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6060:6072 LamSF_Substitution_term <> lift_rec_null thm
R6060:6072 LamSF_Substitution_term <> lift_rec_null thm
R6060:6072 LamSF_Substitution_term <> lift_rec_null thm
R6098:6107 LamSF_Tactics <> multi_step ind
R6121:6123 LamSF_Terms <> App constr
R6126:6128 LamSF_Terms <> App constr
R6109:6118 LamSF_reduction <> lamSF_red1 ind
R6098:6107 LamSF_Tactics <> multi_step ind
R6121:6123 LamSF_Terms <> App constr
R6126:6128 LamSF_Terms <> App constr
R6109:6118 LamSF_reduction <> lamSF_red1 ind
R6172:6174 LamSF_Terms <> App constr
R6177:6179 LamSF_Terms <> App constr
R6182:6184 LamSF_Terms <> App constr
R6191:6194 SF_reduction <> i_op def
R6186:6189 SF_reduction <> k_op def
R6151:6164 LamSF_Tactics <> transitive_red thm
R6172:6174 LamSF_Terms <> App constr
R6177:6179 LamSF_Terms <> App constr
R6182:6184 LamSF_Terms <> App constr
R6191:6194 SF_reduction <> i_op def
R6186:6189 SF_reduction <> k_op def
R6151:6164 LamSF_Tactics <> transitive_red thm
R6217:6239 LamSF_reduction <> preserves_app_lamSF_red thm
R6251:6273 LamSF_reduction <> preserves_app_lamSF_red thm
R6284:6293 Binding <> binds_rank thm
prf 6359:6370 <> binds_star_0
R6393:6397 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6398:6406 LamSF_reduction <> lamSF_red def
R6430:6432 LamSF_Terms <> App constr
R6439:6442 SF_reduction <> i_op def
R6434:6437 SF_reduction <> k_op def
R6409:6411 LamSF_Terms <> App constr
R6420:6423 SF_reduction <> star def
R6425:6425 Binding <> M var
R6413:6417 Binding <> binds def
R6384:6390 LamSF_Closed <> program def
R6392:6392 Binding <> M var
R6482:6485 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6494:6497 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6510:6514 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6515:6523 LamSF_reduction <> lamSF_red def
R6547:6549 LamSF_Terms <> App constr
R6556:6559 SF_reduction <> i_op def
R6551:6554 SF_reduction <> k_op def
R6526:6528 LamSF_Terms <> App constr
R6537:6540 SF_reduction <> star def
R6542:6542 Binding <> M var
R6530:6534 Binding <> binds def
R6506:6508 Coq.Init.Logic <> :type_scope:x_'='_x not
R6498:6503 LamSF_Closed <> maxvar def
R6505:6505 Binding <> M var
R6486:6491 LamSF_Normal <> normal ind
R6493:6493 Binding <> M var
R6477:6480 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6471:6474 LamSF_Tactics <> rank def
R6476:6476 Binding <> M var
R6481:6481 Binding <> p var
R6482:6485 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6494:6497 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6510:6514 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6515:6523 LamSF_reduction <> lamSF_red def
R6547:6549 LamSF_Terms <> App constr
R6556:6559 SF_reduction <> i_op def
R6551:6554 SF_reduction <> k_op def
R6526:6528 LamSF_Terms <> App constr
R6537:6540 SF_reduction <> star def
R6542:6542 Binding <> M var
R6530:6534 Binding <> binds def
R6506:6508 Coq.Init.Logic <> :type_scope:x_'='_x not
R6498:6503 LamSF_Closed <> maxvar def
R6505:6505 Binding <> M var
R6486:6491 LamSF_Normal <> normal ind
R6493:6493 Binding <> M var
R6477:6480 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6471:6474 LamSF_Tactics <> rank def
R6476:6476 Binding <> M var
R6481:6481 Binding <> p var
R6642:6643 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6636:6639 LamSF_Tactics <> rank def
R6642:6643 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6636:6639 LamSF_Tactics <> rank def
R6658:6670 LamSF_Tactics <> rank_positive thm
R6766:6775 Binding <> binds_rank thm
R6813:6817 Binding <> binds def
R6833:6837 Binding <> binds def
R6833:6837 Binding <> binds def
R6847:6854 Binding <> binds_fn def
R6887:6902 LamSF_Closed <> subst_rec_closed thm
R6904:6908 Equal <> equal def
R6887:6902 LamSF_Closed <> subst_rec_closed thm
R6904:6908 Equal <> equal def
R6887:6902 LamSF_Closed <> subst_rec_closed thm
R6904:6908 Equal <> equal def
R6887:6902 LamSF_Closed <> subst_rec_closed thm
R6904:6908 Equal <> equal def
R6887:6902 LamSF_Closed <> subst_rec_closed thm
R6904:6908 Equal <> equal def
R6937:6945 LamSF_Terms <> subst_rec def
R6953:6961 LamSF_Terms <> subst_rec def
R6953:6961 LamSF_Terms <> subst_rec def
R6988:7010 SF_reduction <> lift_rec_preserves_star thm
R6988:7010 SF_reduction <> lift_rec_preserves_star thm
R6988:7010 SF_reduction <> lift_rec_preserves_star thm
R7035:7044 LamSF_Tactics <> multi_step ind
R7058:7060 LamSF_Terms <> App constr
R7063:7065 LamSF_Terms <> App constr
R7046:7055 LamSF_reduction <> lamSF_red1 ind
R7035:7044 LamSF_Tactics <> multi_step ind
R7058:7060 LamSF_Terms <> App constr
R7063:7065 LamSF_Terms <> App constr
R7046:7055 LamSF_reduction <> lamSF_red1 ind
R7109:7111 LamSF_Terms <> App constr
R7114:7116 LamSF_Terms <> App constr
R7119:7121 LamSF_Terms <> App constr
R7128:7131 SF_reduction <> i_op def
R7123:7126 SF_reduction <> k_op def
R7088:7101 LamSF_Tactics <> transitive_red thm
R7109:7111 LamSF_Terms <> App constr
R7114:7116 LamSF_Terms <> App constr
R7119:7121 LamSF_Terms <> App constr
R7128:7131 SF_reduction <> i_op def
R7123:7126 SF_reduction <> k_op def
R7088:7101 LamSF_Tactics <> transitive_red thm
R7154:7176 LamSF_reduction <> preserves_app_lamSF_red thm
R7188:7210 LamSF_reduction <> preserves_app_lamSF_red thm
R7222:7234 LamSF_Substitution_term <> lift_rec_null thm
R7222:7234 LamSF_Substitution_term <> lift_rec_null thm
R7222:7234 LamSF_Substitution_term <> lift_rec_null thm
R7246:7261 Equal <> unequal_programs thm
R7284:7289 LamSF_Normal <> nf_abs constr
R7300:7310 LamSF_Normal <> normal_star thm
R7322:7332 LamSF_Closed <> maxvar_star thm
R7322:7332 LamSF_Closed <> maxvar_star thm
R7322:7332 LamSF_Closed <> maxvar_star thm
R7394:7396 LamSF_Terms <> App constr
R7394:7396 LamSF_Terms <> App constr
R7431:7433 LamSF_Terms <> App constr
R7476:7490 SF_reduction <> right_component def
R7493:7495 LamSF_Terms <> Abs constr
R7498:7501 SF_reduction <> star def
R7436:7438 LamSF_Terms <> App constr
R7443:7456 SF_reduction <> left_component def
R7459:7461 LamSF_Terms <> Abs constr
R7464:7467 SF_reduction <> star def
R7416:7423 LamSF_Tactics <> succ_red constr
R7431:7433 LamSF_Terms <> App constr
R7476:7490 SF_reduction <> right_component def
R7493:7495 LamSF_Terms <> Abs constr
R7498:7501 SF_reduction <> star def
R7436:7438 LamSF_Terms <> App constr
R7443:7456 SF_reduction <> left_component def
R7459:7461 LamSF_Terms <> Abs constr
R7464:7467 SF_reduction <> star def
R7416:7423 LamSF_Tactics <> succ_red constr
R7523:7542 LamSF_reduction <> f_compound_lamSF_red constr
R7554:7574 SF_reduction <> abs_compound_compound constr
R7586:7598 SF_reduction <> star_compound thm
R7633:7648 LamSF_Closed <> subst_rec_closed thm
R7650:7654 Binding <> binds def
R7633:7648 LamSF_Closed <> subst_rec_closed thm
R7650:7654 Binding <> binds def
R7633:7648 LamSF_Closed <> subst_rec_closed thm
R7650:7654 Binding <> binds def
R7633:7648 LamSF_Closed <> subst_rec_closed thm
R7650:7654 Binding <> binds def
R7633:7648 LamSF_Closed <> subst_rec_closed thm
R7650:7654 Binding <> binds def
R7683:7696 SF_reduction <> left_component def
R7699:7713 SF_reduction <> right_component def
R7736:7753 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7736:7753 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7736:7753 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7736:7753 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7736:7753 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7775:7787 LamSF_Substitution_term <> lift_rec_null thm
R7775:7787 LamSF_Substitution_term <> lift_rec_null thm
R7775:7787 LamSF_Substitution_term <> lift_rec_null thm
R7808:7823 LamSF_Closed <> subst_rec_closed thm
R7825:7829 Equal <> equal def
R7808:7823 LamSF_Closed <> subst_rec_closed thm
R7825:7829 Equal <> equal def
R7873:7882 LamSF_Tactics <> multi_step ind
R7896:7898 LamSF_Terms <> App constr
R7901:7903 LamSF_Terms <> App constr
R7884:7893 LamSF_reduction <> lamSF_red1 ind
R7873:7882 LamSF_Tactics <> multi_step ind
R7896:7898 LamSF_Terms <> App constr
R7901:7903 LamSF_Terms <> App constr
R7884:7893 LamSF_reduction <> lamSF_red1 ind
R7947:7949 LamSF_Terms <> App constr
R7952:7954 LamSF_Terms <> App constr
R7957:7959 LamSF_Terms <> App constr
R7966:7969 SF_reduction <> i_op def
R7961:7964 SF_reduction <> k_op def
R7926:7939 LamSF_Tactics <> transitive_red thm
R7947:7949 LamSF_Terms <> App constr
R7952:7954 LamSF_Terms <> App constr
R7957:7959 LamSF_Terms <> App constr
R7966:7969 SF_reduction <> i_op def
R7961:7964 SF_reduction <> k_op def
R7926:7939 LamSF_Tactics <> transitive_red thm
R7992:8014 LamSF_reduction <> preserves_app_lamSF_red thm
R8026:8048 LamSF_reduction <> preserves_app_lamSF_red thm
R8059:8068 Binding <> binds_rank thm
R8141:8143 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8128:8131 LamSF_Tactics <> rank def
R8134:8137 SF_reduction <> star def
R8144:8147 LamSF_Tactics <> rank def
R8150:8152 LamSF_Terms <> Abs constr
R8141:8143 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8128:8131 LamSF_Tactics <> rank def
R8134:8137 SF_reduction <> star def
R8144:8147 LamSF_Tactics <> rank def
R8150:8152 LamSF_Terms <> Abs constr
R8169:8177 SF_reduction <> rank_star thm
R8197:8207 LamSF_Normal <> normal_star thm
R8219:8229 LamSF_Closed <> maxvar_star thm
R8219:8229 LamSF_Closed <> maxvar_star thm
R8219:8229 LamSF_Closed <> maxvar_star thm
R8272:8275 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8254:8259 LamSF_Tactics <> status def
R8262:8264 LamSF_Terms <> App constr
R8276:8281 LamSF_Closed <> maxvar def
R8284:8286 LamSF_Terms <> App constr
R8272:8275 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8254:8259 LamSF_Tactics <> status def
R8262:8264 LamSF_Terms <> App constr
R8276:8281 LamSF_Closed <> maxvar def
R8284:8286 LamSF_Terms <> App constr
R8307:8322 LamSF_Closed <> status_lt_maxvar thm
R8362:8366 Binding <> binds def
R8382:8386 Binding <> binds def
R8382:8386 Binding <> binds def
R8396:8403 Binding <> binds_fn def
R8436:8451 LamSF_Closed <> subst_rec_closed thm
R8453:8457 Equal <> equal def
R8436:8451 LamSF_Closed <> subst_rec_closed thm
R8453:8457 Equal <> equal def
R8436:8451 LamSF_Closed <> subst_rec_closed thm
R8453:8457 Equal <> equal def
R8436:8451 LamSF_Closed <> subst_rec_closed thm
R8453:8457 Equal <> equal def
R8436:8451 LamSF_Closed <> subst_rec_closed thm
R8453:8457 Equal <> equal def
R8486:8494 LamSF_Terms <> subst_rec def
R8502:8510 LamSF_Terms <> subst_rec def
R8502:8510 LamSF_Terms <> subst_rec def
R8537:8554 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8537:8554 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8537:8554 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8537:8554 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8537:8554 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8604:8613 LamSF_Tactics <> multi_step ind
R8627:8629 LamSF_Terms <> App constr
R8632:8634 LamSF_Terms <> App constr
R8615:8624 LamSF_reduction <> lamSF_red1 ind
R8604:8613 LamSF_Tactics <> multi_step ind
R8627:8629 LamSF_Terms <> App constr
R8632:8634 LamSF_Terms <> App constr
R8615:8624 LamSF_reduction <> lamSF_red1 ind
R8678:8680 LamSF_Terms <> App constr
R8683:8685 LamSF_Terms <> App constr
R8688:8690 LamSF_Terms <> App constr
R8697:8700 SF_reduction <> i_op def
R8692:8695 SF_reduction <> k_op def
R8657:8670 LamSF_Tactics <> transitive_red thm
R8678:8680 LamSF_Terms <> App constr
R8683:8685 LamSF_Terms <> App constr
R8688:8690 LamSF_Terms <> App constr
R8697:8700 SF_reduction <> i_op def
R8692:8695 SF_reduction <> k_op def
R8657:8670 LamSF_Tactics <> transitive_red thm
R8723:8745 LamSF_reduction <> preserves_app_lamSF_red thm
R8757:8779 LamSF_reduction <> preserves_app_lamSF_red thm
R8801:8815 LamSF_Closed <> lift_rec_closed thm
R8801:8815 LamSF_Closed <> lift_rec_closed thm
R8801:8815 LamSF_Closed <> lift_rec_closed thm
R8801:8815 LamSF_Closed <> lift_rec_closed thm
R8851:8865 LamSF_Closed <> lift_rec_closed thm
R8851:8865 LamSF_Closed <> lift_rec_closed thm
R8851:8865 LamSF_Closed <> lift_rec_closed thm
R8851:8865 LamSF_Closed <> lift_rec_closed thm
R8901:8916 Equal <> unequal_programs thm
R9040:9055 LamSF_Closed <> subst_rec_closed thm
R9057:9061 Binding <> binds def
R9040:9055 LamSF_Closed <> subst_rec_closed thm
R9057:9061 Binding <> binds def
R9040:9055 LamSF_Closed <> subst_rec_closed thm
R9057:9061 Binding <> binds def
R9040:9055 LamSF_Closed <> subst_rec_closed thm
R9057:9061 Binding <> binds def
R9040:9055 LamSF_Closed <> subst_rec_closed thm
R9057:9061 Binding <> binds def
R9090:9098 LamSF_Terms <> subst_rec def
R9106:9114 LamSF_Terms <> subst_rec def
R9106:9114 LamSF_Terms <> subst_rec def
R9141:9158 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9141:9158 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9141:9158 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9141:9158 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9141:9158 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9208:9217 LamSF_Tactics <> multi_step ind
R9231:9233 LamSF_Terms <> App constr
R9236:9238 LamSF_Terms <> App constr
R9219:9228 LamSF_reduction <> lamSF_red1 ind
R9208:9217 LamSF_Tactics <> multi_step ind
R9231:9233 LamSF_Terms <> App constr
R9236:9238 LamSF_Terms <> App constr
R9219:9228 LamSF_reduction <> lamSF_red1 ind
R9282:9284 LamSF_Terms <> App constr
R9287:9289 LamSF_Terms <> App constr
R9292:9294 LamSF_Terms <> App constr
R9301:9304 SF_reduction <> i_op def
R9296:9299 SF_reduction <> k_op def
R9261:9274 LamSF_Tactics <> transitive_red thm
R9282:9284 LamSF_Terms <> App constr
R9287:9289 LamSF_Terms <> App constr
R9292:9294 LamSF_Terms <> App constr
R9301:9304 SF_reduction <> i_op def
R9296:9299 SF_reduction <> k_op def
R9261:9274 LamSF_Tactics <> transitive_red thm
R9327:9349 LamSF_reduction <> preserves_app_lamSF_red thm
R9361:9383 LamSF_reduction <> preserves_app_lamSF_red thm
R9405:9419 LamSF_Closed <> lift_rec_closed thm
R9405:9419 LamSF_Closed <> lift_rec_closed thm
R9405:9419 LamSF_Closed <> lift_rec_closed thm
R9405:9419 LamSF_Closed <> lift_rec_closed thm
R9476:9480 Binding <> binds def
R9496:9500 Binding <> binds def
R9496:9500 Binding <> binds def
R9510:9517 Binding <> binds_fn def
R9550:9565 LamSF_Closed <> subst_rec_closed thm
R9567:9571 Equal <> equal def
R9550:9565 LamSF_Closed <> subst_rec_closed thm
R9567:9571 Equal <> equal def
R9550:9565 LamSF_Closed <> subst_rec_closed thm
R9567:9571 Equal <> equal def
R9550:9565 LamSF_Closed <> subst_rec_closed thm
R9567:9571 Equal <> equal def
R9550:9565 LamSF_Closed <> subst_rec_closed thm
R9567:9571 Equal <> equal def
R9600:9608 LamSF_Terms <> subst_rec def
R9616:9624 LamSF_Terms <> subst_rec def
R9616:9624 LamSF_Terms <> subst_rec def
R9665:9674 LamSF_Tactics <> multi_step ind
R9688:9690 LamSF_Terms <> App constr
R9693:9695 LamSF_Terms <> App constr
R9676:9685 LamSF_reduction <> lamSF_red1 ind
R9665:9674 LamSF_Tactics <> multi_step ind
R9688:9690 LamSF_Terms <> App constr
R9693:9695 LamSF_Terms <> App constr
R9676:9685 LamSF_reduction <> lamSF_red1 ind
R9739:9741 LamSF_Terms <> App constr
R9744:9746 LamSF_Terms <> App constr
R9749:9751 LamSF_Terms <> App constr
R9758:9761 SF_reduction <> i_op def
R9753:9756 SF_reduction <> k_op def
R9718:9731 LamSF_Tactics <> transitive_red thm
R9739:9741 LamSF_Terms <> App constr
R9744:9746 LamSF_Terms <> App constr
R9749:9751 LamSF_Terms <> App constr
R9758:9761 SF_reduction <> i_op def
R9753:9756 SF_reduction <> k_op def
R9718:9731 LamSF_Tactics <> transitive_red thm
R9784:9806 LamSF_reduction <> preserves_app_lamSF_red thm
R9818:9840 LamSF_reduction <> preserves_app_lamSF_red thm
R9851:9863 LamSF_Substitution_term <> lift_rec_null thm
R9851:9863 LamSF_Substitution_term <> lift_rec_null thm
R9851:9863 LamSF_Substitution_term <> lift_rec_null thm
R9876:9891 Equal <> unequal_programs thm
R9981:9996 LamSF_Closed <> subst_rec_closed thm
R9998:10002 Binding <> binds def
R9981:9996 LamSF_Closed <> subst_rec_closed thm
R9998:10002 Binding <> binds def
R9981:9996 LamSF_Closed <> subst_rec_closed thm
R9998:10002 Binding <> binds def
R9981:9996 LamSF_Closed <> subst_rec_closed thm
R9998:10002 Binding <> binds def
R9981:9996 LamSF_Closed <> subst_rec_closed thm
R9998:10002 Binding <> binds def
R10031:10039 LamSF_Terms <> subst_rec def
R10047:10055 LamSF_Terms <> subst_rec def
R10047:10055 LamSF_Terms <> subst_rec def
R10096:10105 LamSF_Tactics <> multi_step ind
R10119:10121 LamSF_Terms <> App constr
R10124:10126 LamSF_Terms <> App constr
R10107:10116 LamSF_reduction <> lamSF_red1 ind
R10096:10105 LamSF_Tactics <> multi_step ind
R10119:10121 LamSF_Terms <> App constr
R10124:10126 LamSF_Terms <> App constr
R10107:10116 LamSF_reduction <> lamSF_red1 ind
R10170:10172 LamSF_Terms <> App constr
R10175:10177 LamSF_Terms <> App constr
R10180:10182 LamSF_Terms <> App constr
R10189:10192 SF_reduction <> i_op def
R10184:10187 SF_reduction <> k_op def
R10149:10162 LamSF_Tactics <> transitive_red thm
R10170:10172 LamSF_Terms <> App constr
R10175:10177 LamSF_Terms <> App constr
R10180:10182 LamSF_Terms <> App constr
R10189:10192 SF_reduction <> i_op def
R10184:10187 SF_reduction <> k_op def
R10149:10162 LamSF_Tactics <> transitive_red thm
R10215:10237 LamSF_reduction <> preserves_app_lamSF_red thm
R10249:10271 LamSF_reduction <> preserves_app_lamSF_red thm
R10283:10292 Binding <> binds_rank thm
R10356:10360 Binding <> binds def
R10368:10376 LamSF_reduction <> lamSF_red def
R10368:10376 LamSF_reduction <> lamSF_red def
R10392:10396 Binding <> binds def
R10392:10396 Binding <> binds def
R10406:10413 Binding <> binds_fn def
R10446:10461 LamSF_Closed <> subst_rec_closed thm
R10463:10467 Equal <> equal def
R10446:10461 LamSF_Closed <> subst_rec_closed thm
R10463:10467 Equal <> equal def
R10446:10461 LamSF_Closed <> subst_rec_closed thm
R10463:10467 Equal <> equal def
R10446:10461 LamSF_Closed <> subst_rec_closed thm
R10463:10467 Equal <> equal def
R10446:10461 LamSF_Closed <> subst_rec_closed thm
R10463:10467 Equal <> equal def
R10496:10504 LamSF_Terms <> subst_rec def
R10512:10520 LamSF_Terms <> subst_rec def
R10512:10520 LamSF_Terms <> subst_rec def
R10561:10570 LamSF_Tactics <> multi_step ind
R10584:10586 LamSF_Terms <> App constr
R10589:10591 LamSF_Terms <> App constr
R10572:10581 LamSF_reduction <> lamSF_red1 ind
R10561:10570 LamSF_Tactics <> multi_step ind
R10584:10586 LamSF_Terms <> App constr
R10589:10591 LamSF_Terms <> App constr
R10572:10581 LamSF_reduction <> lamSF_red1 ind
R10635:10637 LamSF_Terms <> App constr
R10640:10642 LamSF_Terms <> App constr
R10645:10647 LamSF_Terms <> App constr
R10654:10657 SF_reduction <> i_op def
R10649:10652 SF_reduction <> k_op def
R10614:10627 LamSF_Tactics <> transitive_red thm
R10635:10637 LamSF_Terms <> App constr
R10640:10642 LamSF_Terms <> App constr
R10645:10647 LamSF_Terms <> App constr
R10654:10657 SF_reduction <> i_op def
R10649:10652 SF_reduction <> k_op def
R10614:10627 LamSF_Tactics <> transitive_red thm
R10680:10702 LamSF_reduction <> preserves_app_lamSF_red thm
R10714:10736 LamSF_reduction <> preserves_app_lamSF_red thm
R10747:10759 LamSF_Substitution_term <> lift_rec_null thm
R10747:10759 LamSF_Substitution_term <> lift_rec_null thm
R10747:10759 LamSF_Substitution_term <> lift_rec_null thm
R10772:10787 Equal <> unequal_programs thm
R10861:10863 LamSF_Terms <> App constr
R10861:10863 LamSF_Terms <> App constr
R10898:10900 LamSF_Terms <> App constr
R10937:10951 SF_reduction <> right_component def
R10954:10956 LamSF_Terms <> Abs constr
R10903:10905 LamSF_Terms <> App constr
R10910:10923 SF_reduction <> left_component def
R10926:10928 LamSF_Terms <> Abs constr
R10883:10890 LamSF_Tactics <> succ_red constr
R10898:10900 LamSF_Terms <> App constr
R10937:10951 SF_reduction <> right_component def
R10954:10956 LamSF_Terms <> Abs constr
R10903:10905 LamSF_Terms <> App constr
R10910:10923 SF_reduction <> left_component def
R10926:10928 LamSF_Terms <> Abs constr
R10883:10890 LamSF_Tactics <> succ_red constr
R10978:10997 LamSF_reduction <> f_compound_lamSF_red constr
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11063:11080 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11082:11086 Binding <> binds def
R11109:11122 SF_reduction <> left_component def
R11125:11139 SF_reduction <> right_component def
R11162:11179 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11162:11179 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11162:11179 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11162:11179 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11162:11179 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11202:11214 LamSF_Substitution_term <> lift_rec_null thm
R11202:11214 LamSF_Substitution_term <> lift_rec_null thm
R11202:11214 LamSF_Substitution_term <> lift_rec_null thm
R11226:11238 LamSF_Substitution_term <> lift_rec_null thm
R11226:11238 LamSF_Substitution_term <> lift_rec_null thm
R11226:11238 LamSF_Substitution_term <> lift_rec_null thm
R11264:11273 LamSF_Tactics <> multi_step ind
R11287:11289 LamSF_Terms <> App constr
R11292:11294 LamSF_Terms <> App constr
R11275:11284 LamSF_reduction <> lamSF_red1 ind
R11264:11273 LamSF_Tactics <> multi_step ind
R11287:11289 LamSF_Terms <> App constr
R11292:11294 LamSF_Terms <> App constr
R11275:11284 LamSF_reduction <> lamSF_red1 ind
R11338:11340 LamSF_Terms <> App constr
R11343:11345 LamSF_Terms <> App constr
R11348:11350 LamSF_Terms <> App constr
R11357:11360 SF_reduction <> i_op def
R11352:11355 SF_reduction <> k_op def
R11317:11330 LamSF_Tactics <> transitive_red thm
R11338:11340 LamSF_Terms <> App constr
R11343:11345 LamSF_Terms <> App constr
R11348:11350 LamSF_Terms <> App constr
R11357:11360 SF_reduction <> i_op def
R11352:11355 SF_reduction <> k_op def
R11317:11330 LamSF_Tactics <> transitive_red thm
R11383:11405 LamSF_reduction <> preserves_app_lamSF_red thm
R11417:11439 LamSF_reduction <> preserves_app_lamSF_red thm
R11451:11460 Binding <> binds_rank thm
R11591:11595 Binding <> binds def
R11603:11611 LamSF_reduction <> lamSF_red def
R11603:11611 LamSF_reduction <> lamSF_red def
R11627:11631 Binding <> binds def
R11627:11631 Binding <> binds def
R11641:11648 Binding <> binds_fn def
R11681:11696 LamSF_Closed <> subst_rec_closed thm
R11698:11702 Equal <> equal def
R11681:11696 LamSF_Closed <> subst_rec_closed thm
R11698:11702 Equal <> equal def
R11681:11696 LamSF_Closed <> subst_rec_closed thm
R11698:11702 Equal <> equal def
R11681:11696 LamSF_Closed <> subst_rec_closed thm
R11698:11702 Equal <> equal def
R11681:11696 LamSF_Closed <> subst_rec_closed thm
R11698:11702 Equal <> equal def
R11731:11739 LamSF_Terms <> subst_rec def
R11747:11755 LamSF_Terms <> subst_rec def
R11747:11755 LamSF_Terms <> subst_rec def
R11796:11805 LamSF_Tactics <> multi_step ind
R11819:11821 LamSF_Terms <> App constr
R11824:11826 LamSF_Terms <> App constr
R11807:11816 LamSF_reduction <> lamSF_red1 ind
R11796:11805 LamSF_Tactics <> multi_step ind
R11819:11821 LamSF_Terms <> App constr
R11824:11826 LamSF_Terms <> App constr
R11807:11816 LamSF_reduction <> lamSF_red1 ind
R11870:11872 LamSF_Terms <> App constr
R11875:11877 LamSF_Terms <> App constr
R11880:11882 LamSF_Terms <> App constr
R11889:11892 SF_reduction <> i_op def
R11884:11887 SF_reduction <> k_op def
R11849:11862 LamSF_Tactics <> transitive_red thm
R11870:11872 LamSF_Terms <> App constr
R11875:11877 LamSF_Terms <> App constr
R11880:11882 LamSF_Terms <> App constr
R11889:11892 SF_reduction <> i_op def
R11884:11887 SF_reduction <> k_op def
R11849:11862 LamSF_Tactics <> transitive_red thm
R11915:11937 LamSF_reduction <> preserves_app_lamSF_red thm
R11949:11971 LamSF_reduction <> preserves_app_lamSF_red thm
R11982:11994 LamSF_Substitution_term <> lift_rec_null thm
R11982:11994 LamSF_Substitution_term <> lift_rec_null thm
R11982:11994 LamSF_Substitution_term <> lift_rec_null thm
R12007:12022 Equal <> unequal_programs thm
R12095:12097 LamSF_Terms <> App constr
R12095:12097 LamSF_Terms <> App constr
R12132:12134 LamSF_Terms <> App constr
R12171:12185 SF_reduction <> right_component def
R12188:12190 LamSF_Terms <> Abs constr
R12137:12139 LamSF_Terms <> App constr
R12144:12157 SF_reduction <> left_component def
R12160:12162 LamSF_Terms <> Abs constr
R12117:12124 LamSF_Tactics <> succ_red constr
R12132:12134 LamSF_Terms <> App constr
R12171:12185 SF_reduction <> right_component def
R12188:12190 LamSF_Terms <> Abs constr
R12137:12139 LamSF_Terms <> App constr
R12144:12157 SF_reduction <> left_component def
R12160:12162 LamSF_Terms <> Abs constr
R12117:12124 LamSF_Tactics <> succ_red constr
R12212:12231 LamSF_reduction <> f_compound_lamSF_red constr
R12242:12251 LamSF_Closed <> factorable def
R12254:12256 LamSF_Terms <> Abs constr
R12242:12251 LamSF_Closed <> factorable def
R12254:12256 LamSF_Terms <> Abs constr
R12273:12295 LamSF_Closed <> programs_are_factorable thm
R12373:12388 LamSF_Closed <> subst_rec_closed thm
R12390:12394 Binding <> binds def
R12373:12388 LamSF_Closed <> subst_rec_closed thm
R12390:12394 Binding <> binds def
R12373:12388 LamSF_Closed <> subst_rec_closed thm
R12390:12394 Binding <> binds def
R12373:12388 LamSF_Closed <> subst_rec_closed thm
R12390:12394 Binding <> binds def
R12373:12388 LamSF_Closed <> subst_rec_closed thm
R12390:12394 Binding <> binds def
R12423:12436 SF_reduction <> left_component def
R12439:12453 SF_reduction <> right_component def
R12476:12493 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12476:12493 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12476:12493 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12476:12493 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12476:12493 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12516:12528 LamSF_Substitution_term <> lift_rec_null thm
R12516:12528 LamSF_Substitution_term <> lift_rec_null thm
R12516:12528 LamSF_Substitution_term <> lift_rec_null thm
R12554:12563 LamSF_Tactics <> multi_step ind
R12577:12579 LamSF_Terms <> App constr
R12582:12584 LamSF_Terms <> App constr
R12565:12574 LamSF_reduction <> lamSF_red1 ind
R12554:12563 LamSF_Tactics <> multi_step ind
R12577:12579 LamSF_Terms <> App constr
R12582:12584 LamSF_Terms <> App constr
R12565:12574 LamSF_reduction <> lamSF_red1 ind
R12628:12630 LamSF_Terms <> App constr
R12633:12635 LamSF_Terms <> App constr
R12638:12640 LamSF_Terms <> App constr
R12647:12650 SF_reduction <> i_op def
R12642:12645 SF_reduction <> k_op def
R12607:12620 LamSF_Tactics <> transitive_red thm
R12628:12630 LamSF_Terms <> App constr
R12633:12635 LamSF_Terms <> App constr
R12638:12640 LamSF_Terms <> App constr
R12647:12650 SF_reduction <> i_op def
R12642:12645 SF_reduction <> k_op def
R12607:12620 LamSF_Tactics <> transitive_red thm
R12673:12695 LamSF_reduction <> preserves_app_lamSF_red thm
R12707:12729 LamSF_reduction <> preserves_app_lamSF_red thm
R12741:12750 Binding <> binds_rank thm
prf 12848:12859 <> binds_star_1
R12881:12884 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12897:12901 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12902:12910 LamSF_reduction <> lamSF_red def
R12933:12936 SF_reduction <> k_op def
R12913:12915 LamSF_Terms <> App constr
R12924:12927 SF_reduction <> star def
R12929:12929 Binding <> M var
R12917:12921 Binding <> binds def
R12893:12895 Coq.Init.Logic <> :type_scope:x_'='_x not
R12885:12890 LamSF_Closed <> maxvar def
R12892:12892 Binding <> M var
R12873:12878 LamSF_Normal <> normal ind
R12880:12880 Binding <> M var
R12975:12978 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12987:12990 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13003:13007 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13008:13016 LamSF_reduction <> lamSF_red def