forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathUnstar.glob
1559 lines (1559 loc) · 61 KB
/
Unstar.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 dd75069978c82feecca2c705ff96b25e
FUnstar
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:2391 Eta <> <> lib
R2409:2413 Equal <> <> lib
R2431:2441 Combinators <> <> lib
R2459:2465 Binding <> <> lib
R2483:2487 Coq.omega.Omega <> <> lib
def 2821:2829 <> unstar_fn
R2835:2837 LamSF_Terms <> Abs constr
R2840:2842 LamSF_Terms <> Abs constr
R2845:2847 LamSF_Terms <> App constr
R2883:2885 LamSF_Terms <> Abs constr
R2888:2890 LamSF_Terms <> Abs constr
R2894:2896 LamSF_Terms <> App constr
R2982:2984 LamSF_Terms <> App constr
R3044:3046 LamSF_Terms <> App constr
R3082:3084 LamSF_Terms <> Abs constr
R3087:3089 LamSF_Terms <> Abs constr
R3093:3095 LamSF_Terms <> App constr
R3118:3120 LamSF_Terms <> Ref constr
R3098:3100 LamSF_Terms <> App constr
R3109:3111 LamSF_Terms <> Ref constr
R3102:3106 Combinators <> abs_S def
R3049:3051 LamSF_Terms <> App constr
R3073:3075 LamSF_Terms <> Ref constr
R3054:3056 LamSF_Terms <> App constr
R3064:3066 LamSF_Terms <> Ref constr
R3058:3061 SF_reduction <> f_op def
R2987:2989 LamSF_Terms <> App constr
R3023:3025 LamSF_Terms <> App constr
R3034:3036 LamSF_Terms <> Ref constr
R3027:3031 Combinators <> abs_K def
R2992:2994 LamSF_Terms <> App constr
R3014:3016 LamSF_Terms <> Ref constr
R2997:2999 LamSF_Terms <> App constr
R3007:3010 SF_reduction <> k_op def
R3001:3005 Equal <> equal def
R2899:2901 LamSF_Terms <> App constr
R2939:2941 LamSF_Terms <> Abs constr
R2944:2946 LamSF_Terms <> App constr
R2957:2959 LamSF_Terms <> App constr
R2970:2972 LamSF_Terms <> Ref constr
R2962:2964 LamSF_Terms <> Ref constr
R2949:2951 LamSF_Terms <> Ref constr
R2904:2906 LamSF_Terms <> App constr
R2930:2932 LamSF_Terms <> Ref constr
R2909:2911 LamSF_Terms <> App constr
R2919:2926 SF_reduction <> abs_left def
R2913:2917 Equal <> equal def
R2850:2852 LamSF_Terms <> App constr
R2874:2876 LamSF_Terms <> Ref constr
R2855:2857 LamSF_Terms <> App constr
R2865:2867 LamSF_Terms <> Ref constr
R2859:2862 SF_reduction <> f_op def
def 3150:3155 <> unstar
R3160:3162 LamSF_Terms <> App constr
R3173:3181 Unstar <> unstar_fn def
R3164:3171 LamSF_Eval <> fixpoint def
prf 3194:3204 <> unstar_star
R3226:3229 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3230:3238 LamSF_reduction <> lamSF_red def
R3263:3265 LamSF_Terms <> Abs constr
R3267:3267 Unstar <> M var
R3241:3243 LamSF_Terms <> App constr
R3253:3256 SF_reduction <> star def
R3258:3258 Unstar <> M var
R3245:3250 Unstar <> unstar def
R3218:3223 LamSF_Normal <> normal ind
R3225:3225 Unstar <> M var
R3321:3326 Unstar <> unstar def
R3342:3347 Unstar <> unstar def
R3342:3347 Unstar <> unstar def
R3357:3365 Unstar <> unstar_fn def
R3417:3425 LamSF_Terms <> subst_rec def
R3433:3441 LamSF_Terms <> subst_rec def
R3433:3441 LamSF_Terms <> subst_rec def
R3503:3518 LamSF_Closed <> subst_rec_closed thm
R3520:3524 Equal <> equal def
R3503:3518 LamSF_Closed <> subst_rec_closed thm
R3520:3524 Equal <> equal def
R3503:3518 LamSF_Closed <> subst_rec_closed thm
R3520:3524 Equal <> equal def
R3503:3518 LamSF_Closed <> subst_rec_closed thm
R3520:3524 Equal <> equal def
R3503:3518 LamSF_Closed <> subst_rec_closed thm
R3520:3524 Equal <> equal def
R3563:3578 LamSF_Closed <> subst_rec_closed thm
R3580:3585 Unstar <> unstar def
R3563:3578 LamSF_Closed <> subst_rec_closed thm
R3580:3585 Unstar <> unstar def
R3563:3578 LamSF_Closed <> subst_rec_closed thm
R3580:3585 Unstar <> unstar def
R3563:3578 LamSF_Closed <> subst_rec_closed thm
R3580:3585 Unstar <> unstar def
R3563:3578 LamSF_Closed <> subst_rec_closed thm
R3580:3585 Unstar <> unstar def
R3614:3622 LamSF_Terms <> subst_rec def
R3630:3638 LamSF_Terms <> subst_rec def
R3630:3638 LamSF_Terms <> subst_rec def
R3674:3689 LamSF_Closed <> subst_rec_closed thm
R3691:3695 Combinators <> abs_K def
R3674:3689 LamSF_Closed <> subst_rec_closed thm
R3691:3695 Combinators <> abs_K def
R3674:3689 LamSF_Closed <> subst_rec_closed thm
R3691:3695 Combinators <> abs_K def
R3674:3689 LamSF_Closed <> subst_rec_closed thm
R3691:3695 Combinators <> abs_K def
R3674:3689 LamSF_Closed <> subst_rec_closed thm
R3691:3695 Combinators <> abs_K def
R3739:3748 LamSF_Tactics <> multi_step ind
R3762:3764 LamSF_Terms <> App constr
R3767:3769 LamSF_Terms <> App constr
R3750:3759 LamSF_reduction <> lamSF_red1 ind
R3739:3748 LamSF_Tactics <> multi_step ind
R3762:3764 LamSF_Terms <> App constr
R3767:3769 LamSF_Terms <> App constr
R3750:3759 LamSF_reduction <> lamSF_red1 ind
R3813:3815 LamSF_Terms <> App constr
R3818:3820 LamSF_Terms <> App constr
R3823:3825 LamSF_Terms <> App constr
R3832:3835 SF_reduction <> i_op def
R3827:3830 SF_reduction <> k_op def
R3792:3805 LamSF_Tactics <> transitive_red thm
R3813:3815 LamSF_Terms <> App constr
R3818:3820 LamSF_Terms <> App constr
R3823:3825 LamSF_Terms <> App constr
R3832:3835 SF_reduction <> i_op def
R3827:3830 SF_reduction <> k_op def
R3792:3805 LamSF_Tactics <> transitive_red thm
R3858:3880 LamSF_reduction <> preserves_app_lamSF_red thm
R3892:3914 LamSF_reduction <> preserves_app_lamSF_red thm
R3926:3941 Equal <> unequal_programs thm
R4003:4012 LamSF_Tactics <> multi_step ind
R4026:4028 LamSF_Terms <> App constr
R4031:4033 LamSF_Terms <> App constr
R4014:4023 LamSF_reduction <> lamSF_red1 ind
R4003:4012 LamSF_Tactics <> multi_step ind
R4026:4028 LamSF_Terms <> App constr
R4031:4033 LamSF_Terms <> App constr
R4014:4023 LamSF_reduction <> lamSF_red1 ind
R4077:4079 LamSF_Terms <> App constr
R4082:4084 LamSF_Terms <> App constr
R4087:4089 LamSF_Terms <> App constr
R4096:4099 SF_reduction <> i_op def
R4091:4094 SF_reduction <> k_op def
R4056:4069 LamSF_Tactics <> transitive_red thm
R4077:4079 LamSF_Terms <> App constr
R4082:4084 LamSF_Terms <> App constr
R4087:4089 LamSF_Terms <> App constr
R4096:4099 SF_reduction <> i_op def
R4091:4094 SF_reduction <> k_op def
R4056:4069 LamSF_Tactics <> transitive_red thm
R4122:4144 LamSF_reduction <> preserves_app_lamSF_red thm
R4156:4178 LamSF_reduction <> preserves_app_lamSF_red thm
R4190:4205 Equal <> unequal_programs thm
R4287:4302 LamSF_Closed <> subst_rec_closed thm
R4304:4308 Combinators <> abs_S def
R4287:4302 LamSF_Closed <> subst_rec_closed thm
R4304:4308 Combinators <> abs_S def
R4287:4302 LamSF_Closed <> subst_rec_closed thm
R4304:4308 Combinators <> abs_S def
R4287:4302 LamSF_Closed <> subst_rec_closed thm
R4304:4308 Combinators <> abs_S def
R4287:4302 LamSF_Closed <> subst_rec_closed thm
R4304:4308 Combinators <> abs_S def
R4337:4341 Combinators <> abs_S def
R4365:4373 LamSF_Terms <> subst_rec def
R4381:4389 LamSF_Terms <> subst_rec def
R4381:4389 LamSF_Terms <> subst_rec def
R4416:4438 LamSF_reduction <> preserves_abs_lamSF_red thm
R4471:4479 LamSF_Terms <> subst_rec def
R4487:4495 LamSF_Terms <> subst_rec def
R4487:4495 LamSF_Terms <> subst_rec def
R4556:4571 LamSF_Closed <> subst_rec_closed thm
R4573:4577 Equal <> equal def
R4556:4571 LamSF_Closed <> subst_rec_closed thm
R4573:4577 Equal <> equal def
R4556:4571 LamSF_Closed <> subst_rec_closed thm
R4573:4577 Equal <> equal def
R4556:4571 LamSF_Closed <> subst_rec_closed thm
R4573:4577 Equal <> equal def
R4556:4571 LamSF_Closed <> subst_rec_closed thm
R4573:4577 Equal <> equal def
R4606:4614 LamSF_Terms <> subst_rec def
R4622:4630 LamSF_Terms <> subst_rec def
R4622:4630 LamSF_Terms <> subst_rec def
R4671:4680 LamSF_Tactics <> multi_step ind
R4694:4696 LamSF_Terms <> App constr
R4699:4701 LamSF_Terms <> App constr
R4682:4691 LamSF_reduction <> lamSF_red1 ind
R4671:4680 LamSF_Tactics <> multi_step ind
R4694:4696 LamSF_Terms <> App constr
R4699:4701 LamSF_Terms <> App constr
R4682:4691 LamSF_reduction <> lamSF_red1 ind
R4745:4747 LamSF_Terms <> App constr
R4750:4752 LamSF_Terms <> App constr
R4755:4757 LamSF_Terms <> App constr
R4764:4767 SF_reduction <> i_op def
R4759:4762 SF_reduction <> k_op def
R4724:4737 LamSF_Tactics <> transitive_red thm
R4745:4747 LamSF_Terms <> App constr
R4750:4752 LamSF_Terms <> App constr
R4755:4757 LamSF_Terms <> App constr
R4764:4767 SF_reduction <> i_op def
R4759:4762 SF_reduction <> k_op def
R4724:4737 LamSF_Tactics <> transitive_red thm
R4790:4812 LamSF_reduction <> preserves_app_lamSF_red thm
R4824:4846 LamSF_reduction <> preserves_app_lamSF_red thm
R4858:4873 Equal <> unequal_programs thm
R4935:4944 LamSF_Tactics <> multi_step ind
R4958:4960 LamSF_Terms <> App constr
R4963:4965 LamSF_Terms <> App constr
R4946:4955 LamSF_reduction <> lamSF_red1 ind
R4935:4944 LamSF_Tactics <> multi_step ind
R4958:4960 LamSF_Terms <> App constr
R4963:4965 LamSF_Terms <> App constr
R4946:4955 LamSF_reduction <> lamSF_red1 ind
R5009:5011 LamSF_Terms <> App constr
R5014:5016 LamSF_Terms <> App constr
R5018:5021 SF_reduction <> k_op def
R4988:5001 LamSF_Tactics <> transitive_red thm
R5009:5011 LamSF_Terms <> App constr
R5014:5016 LamSF_Terms <> App constr
R5018:5021 SF_reduction <> k_op def
R4988:5001 LamSF_Tactics <> transitive_red thm
R5043:5065 LamSF_reduction <> preserves_app_lamSF_red thm
R5077:5099 LamSF_reduction <> preserves_app_lamSF_red thm
R5111:5124 Equal <> equal_programs thm
R5170:5185 LamSF_Closed <> subst_rec_closed thm
R5187:5191 Combinators <> abs_K def
R5170:5185 LamSF_Closed <> subst_rec_closed thm
R5187:5191 Combinators <> abs_K def
R5170:5185 LamSF_Closed <> subst_rec_closed thm
R5187:5191 Combinators <> abs_K def
R5170:5185 LamSF_Closed <> subst_rec_closed thm
R5187:5191 Combinators <> abs_K def
R5170:5185 LamSF_Closed <> subst_rec_closed thm
R5187:5191 Combinators <> abs_K def
R5220:5224 Combinators <> abs_K def
R5285:5290 Unstar <> unstar def
R5306:5311 Unstar <> unstar def
R5306:5311 Unstar <> unstar def
R5321:5329 Unstar <> unstar_fn def
R5352:5360 LamSF_Terms <> subst_rec def
R5368:5376 LamSF_Terms <> subst_rec def
R5368:5376 LamSF_Terms <> subst_rec def
R5438:5453 LamSF_Closed <> subst_rec_closed thm
R5455:5459 Equal <> equal def
R5438:5453 LamSF_Closed <> subst_rec_closed thm
R5455:5459 Equal <> equal def
R5438:5453 LamSF_Closed <> subst_rec_closed thm
R5455:5459 Equal <> equal def
R5438:5453 LamSF_Closed <> subst_rec_closed thm
R5455:5459 Equal <> equal def
R5438:5453 LamSF_Closed <> subst_rec_closed thm
R5455:5459 Equal <> equal def
R5498:5513 LamSF_Closed <> subst_rec_closed thm
R5515:5520 Unstar <> unstar def
R5498:5513 LamSF_Closed <> subst_rec_closed thm
R5515:5520 Unstar <> unstar def
R5498:5513 LamSF_Closed <> subst_rec_closed thm
R5515:5520 Unstar <> unstar def
R5498:5513 LamSF_Closed <> subst_rec_closed thm
R5515:5520 Unstar <> unstar def
R5498:5513 LamSF_Closed <> subst_rec_closed thm
R5515:5520 Unstar <> unstar def
R5549:5557 LamSF_Terms <> subst_rec def
R5565:5573 LamSF_Terms <> subst_rec def
R5565:5573 LamSF_Terms <> subst_rec def
R5614:5623 LamSF_Tactics <> multi_step ind
R5637:5639 LamSF_Terms <> App constr
R5642:5644 LamSF_Terms <> App constr
R5625:5634 LamSF_reduction <> lamSF_red1 ind
R5614:5623 LamSF_Tactics <> multi_step ind
R5637:5639 LamSF_Terms <> App constr
R5642:5644 LamSF_Terms <> App constr
R5625:5634 LamSF_reduction <> lamSF_red1 ind
R5688:5690 LamSF_Terms <> App constr
R5693:5695 LamSF_Terms <> App constr
R5698:5700 LamSF_Terms <> App constr
R5707:5710 SF_reduction <> i_op def
R5702:5705 SF_reduction <> k_op def
R5667:5680 LamSF_Tactics <> transitive_red thm
R5688:5690 LamSF_Terms <> App constr
R5693:5695 LamSF_Terms <> App constr
R5698:5700 LamSF_Terms <> App constr
R5707:5710 SF_reduction <> i_op def
R5702:5705 SF_reduction <> k_op def
R5667:5680 LamSF_Tactics <> transitive_red thm
R5733:5755 LamSF_reduction <> preserves_app_lamSF_red thm
R5767:5789 LamSF_reduction <> preserves_app_lamSF_red thm
R5801:5816 Equal <> unequal_programs thm
R5878:5887 LamSF_Tactics <> multi_step ind
R5901:5903 LamSF_Terms <> App constr
R5906:5908 LamSF_Terms <> App constr
R5889:5898 LamSF_reduction <> lamSF_red1 ind
R5878:5887 LamSF_Tactics <> multi_step ind
R5901:5903 LamSF_Terms <> App constr
R5906:5908 LamSF_Terms <> App constr
R5889:5898 LamSF_reduction <> lamSF_red1 ind
R5952:5954 LamSF_Terms <> App constr
R5957:5959 LamSF_Terms <> App constr
R5961:5964 SF_reduction <> k_op def
R5931:5944 LamSF_Tactics <> transitive_red thm
R5952:5954 LamSF_Terms <> App constr
R5957:5959 LamSF_Terms <> App constr
R5961:5964 SF_reduction <> k_op def
R5931:5944 LamSF_Tactics <> transitive_red thm
R5986:6008 LamSF_reduction <> preserves_app_lamSF_red thm
R6020:6042 LamSF_reduction <> preserves_app_lamSF_red thm
R6054:6067 Equal <> equal_programs thm
R6113:6128 LamSF_Closed <> subst_rec_closed thm
R6130:6134 Combinators <> abs_K def
R6113:6128 LamSF_Closed <> subst_rec_closed thm
R6130:6134 Combinators <> abs_K def
R6113:6128 LamSF_Closed <> subst_rec_closed thm
R6130:6134 Combinators <> abs_K def
R6113:6128 LamSF_Closed <> subst_rec_closed thm
R6130:6134 Combinators <> abs_K def
R6113:6128 LamSF_Closed <> subst_rec_closed thm
R6130:6134 Combinators <> abs_K def
R6163:6167 Combinators <> abs_K def
R6205:6210 Unstar <> unstar def
R6226:6231 Unstar <> unstar def
R6226:6231 Unstar <> unstar def
R6241:6249 Unstar <> unstar_fn def
R6272:6280 LamSF_Terms <> subst_rec def
R6288:6296 LamSF_Terms <> subst_rec def
R6288:6296 LamSF_Terms <> subst_rec def
R6338:6347 LamSF_Tactics <> multi_step ind
R6361:6363 LamSF_Terms <> App constr
R6366:6368 LamSF_Terms <> App constr
R6371:6373 LamSF_Terms <> App constr
R6376:6377 LamSF_Terms <> Op constr
R6379:6381 LamSF_Terms <> Fop constr
R6349:6358 LamSF_reduction <> lamSF_red1 ind
R6338:6347 LamSF_Tactics <> multi_step ind
R6361:6363 LamSF_Terms <> App constr
R6366:6368 LamSF_Terms <> App constr
R6371:6373 LamSF_Terms <> App constr
R6376:6377 LamSF_Terms <> Op constr
R6379:6381 LamSF_Terms <> Fop constr
R6349:6358 LamSF_reduction <> lamSF_red1 ind
R6422:6424 LamSF_Terms <> App constr
R6455:6469 SF_reduction <> right_component def
R6427:6429 LamSF_Terms <> App constr
R6434:6447 SF_reduction <> left_component def
R6407:6414 LamSF_Tactics <> succ_red constr
R6422:6424 LamSF_Terms <> App constr
R6455:6469 SF_reduction <> right_component def
R6427:6429 LamSF_Terms <> App constr
R6434:6447 SF_reduction <> left_component def
R6407:6414 LamSF_Tactics <> succ_red constr
R6489:6508 LamSF_reduction <> f_compound_lamSF_red constr
R6520:6542 SF_reduction <> lift_rec_preserves_star thm
R6520:6542 SF_reduction <> lift_rec_preserves_star thm
R6520:6542 SF_reduction <> lift_rec_preserves_star thm
R6553:6565 LamSF_Substitution_term <> lift_rec_null thm
R6553:6565 LamSF_Substitution_term <> lift_rec_null thm
R6553:6565 LamSF_Substitution_term <> lift_rec_null thm
R6577:6597 SF_reduction <> abs_compound_compound constr
R6609:6621 SF_reduction <> star_compound thm
R6655:6670 LamSF_Closed <> subst_rec_closed thm
R6672:6676 Equal <> equal def
R6655:6670 LamSF_Closed <> subst_rec_closed thm
R6672:6676 Equal <> equal def
R6655:6670 LamSF_Closed <> subst_rec_closed thm
R6672:6676 Equal <> equal def
R6655:6670 LamSF_Closed <> subst_rec_closed thm
R6672:6676 Equal <> equal def
R6655:6670 LamSF_Closed <> subst_rec_closed thm
R6672:6676 Equal <> equal def
R6704:6717 SF_reduction <> left_component def
R6725:6738 SF_reduction <> left_component def
R6725:6738 SF_reduction <> left_component def
R6751:6765 LamSF_Closed <> lift_rec_closed thm
R6751:6765 LamSF_Closed <> lift_rec_closed thm
R6751:6765 LamSF_Closed <> lift_rec_closed thm
R6751:6765 LamSF_Closed <> lift_rec_closed thm
R6792:6807 LamSF_Closed <> subst_rec_closed thm
R6792:6807 LamSF_Closed <> subst_rec_closed thm
R6792:6807 LamSF_Closed <> subst_rec_closed thm
R6792:6807 LamSF_Closed <> subst_rec_closed thm
R6847:6856 LamSF_Tactics <> multi_step ind
R6870:6872 LamSF_Terms <> App constr
R6875:6877 LamSF_Terms <> App constr
R6858:6867 LamSF_reduction <> lamSF_red1 ind
R6847:6856 LamSF_Tactics <> multi_step ind
R6870:6872 LamSF_Terms <> App constr
R6875:6877 LamSF_Terms <> App constr
R6858:6867 LamSF_reduction <> lamSF_red1 ind
R6921:6923 LamSF_Terms <> App constr
R6926:6928 LamSF_Terms <> App constr
R6930:6933 SF_reduction <> k_op def
R6900:6913 LamSF_Tactics <> transitive_red thm
R6921:6923 LamSF_Terms <> App constr
R6926:6928 LamSF_Terms <> App constr
R6930:6933 SF_reduction <> k_op def
R6900:6913 LamSF_Tactics <> transitive_red thm
R6955:6977 LamSF_reduction <> preserves_app_lamSF_red thm
R6989:7011 LamSF_reduction <> preserves_app_lamSF_red thm
R7035:7048 Equal <> equal_programs thm
R7083:7105 LamSF_reduction <> preserves_abs_lamSF_red thm
R7117:7134 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7117:7134 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7117:7134 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7117:7134 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7117:7134 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7157:7174 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7157:7174 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7157:7174 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7157:7174 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7157:7174 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7197:7214 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7197:7214 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7197:7214 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7197:7214 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7197:7214 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7237:7251 LamSF_Closed <> lift_rec_closed thm
R7237:7251 LamSF_Closed <> lift_rec_closed thm
R7237:7251 LamSF_Closed <> lift_rec_closed thm
R7237:7251 LamSF_Closed <> lift_rec_closed thm
R7277:7294 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7277:7294 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7277:7294 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7277:7294 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7277:7294 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7317:7334 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7317:7334 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7317:7334 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7317:7334 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7317:7334 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7376:7378 LamSF_Terms <> App constr
R7388:7391 SF_reduction <> star def
R7380:7385 Unstar <> unstar def
R7355:7368 LamSF_Tactics <> transitive_red thm
R7376:7378 LamSF_Terms <> App constr
R7388:7391 SF_reduction <> star def
R7380:7385 Unstar <> unstar def
R7355:7368 LamSF_Tactics <> transitive_red thm
R7406:7428 LamSF_reduction <> preserves_app_lamSF_red thm
R7453:7471 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7453:7471 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7453:7471 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7524:7529 Unstar <> unstar def
R7545:7550 Unstar <> unstar def
R7545:7550 Unstar <> unstar def
R7560:7568 Unstar <> unstar_fn def
R7591:7599 LamSF_Terms <> subst_rec def
R7607:7615 LamSF_Terms <> subst_rec def
R7607:7615 LamSF_Terms <> subst_rec def
R7677:7692 LamSF_Closed <> subst_rec_closed thm
R7694:7698 Equal <> equal def
R7677:7692 LamSF_Closed <> subst_rec_closed thm
R7694:7698 Equal <> equal def
R7677:7692 LamSF_Closed <> subst_rec_closed thm
R7694:7698 Equal <> equal def
R7677:7692 LamSF_Closed <> subst_rec_closed thm
R7694:7698 Equal <> equal def
R7677:7692 LamSF_Closed <> subst_rec_closed thm
R7694:7698 Equal <> equal def
R7726:7734 LamSF_Terms <> subst_rec def
R7742:7750 LamSF_Terms <> subst_rec def
R7742:7750 LamSF_Terms <> subst_rec def
R7792:7801 LamSF_Tactics <> multi_step ind
R7815:7817 LamSF_Terms <> App constr
R7820:7822 LamSF_Terms <> App constr
R7803:7812 LamSF_reduction <> lamSF_red1 ind
R7792:7801 LamSF_Tactics <> multi_step ind
R7815:7817 LamSF_Terms <> App constr
R7820:7822 LamSF_Terms <> App constr
R7803:7812 LamSF_reduction <> lamSF_red1 ind
R7866:7868 LamSF_Terms <> App constr
R7871:7873 LamSF_Terms <> App constr
R7876:7878 LamSF_Terms <> App constr
R7885:7888 SF_reduction <> i_op def
R7880:7883 SF_reduction <> k_op def
R7845:7858 LamSF_Tactics <> transitive_red thm
R7866:7868 LamSF_Terms <> App constr
R7871:7873 LamSF_Terms <> App constr
R7876:7878 LamSF_Terms <> App constr
R7885:7888 SF_reduction <> i_op def
R7880:7883 SF_reduction <> k_op def
R7845:7858 LamSF_Tactics <> transitive_red thm
R7911:7933 LamSF_reduction <> preserves_app_lamSF_red thm
R7945:7967 LamSF_reduction <> preserves_app_lamSF_red thm
R7992:8000 LamSF_reduction <> lamSF_red def
R8003:8005 LamSF_Terms <> App constr
R8008:8010 LamSF_Terms <> App constr
R7992:8000 LamSF_reduction <> lamSF_red def
R8003:8005 LamSF_Terms <> App constr
R8008:8010 LamSF_Terms <> App constr
R8056:8058 LamSF_Terms <> App constr
R8182:8184 LamSF_Terms <> App constr
R8191:8194 SF_reduction <> i_op def
R8186:8189 SF_reduction <> k_op def
R8061:8063 LamSF_Terms <> App constr
R8123:8125 LamSF_Terms <> App constr
R8160:8174 SF_reduction <> right_component def
R8128:8130 LamSF_Terms <> App constr
R8139:8153 SF_reduction <> right_component def
R8132:8136 Equal <> equal def
R8066:8068 LamSF_Terms <> App constr
R8102:8115 SF_reduction <> left_component def
R8071:8073 LamSF_Terms <> App constr
R8082:8095 SF_reduction <> left_component def
R8075:8079 Equal <> equal def
R8034:8047 LamSF_Tactics <> transitive_red thm
R8056:8058 LamSF_Terms <> App constr
R8182:8184 LamSF_Terms <> App constr
R8191:8194 SF_reduction <> i_op def
R8186:8189 SF_reduction <> k_op def
R8061:8063 LamSF_Terms <> App constr
R8123:8125 LamSF_Terms <> App constr
R8160:8174 SF_reduction <> right_component def
R8128:8130 LamSF_Terms <> App constr
R8139:8153 SF_reduction <> right_component def
R8132:8136 Equal <> equal def
R8066:8068 LamSF_Terms <> App constr
R8102:8115 SF_reduction <> left_component def
R8071:8073 LamSF_Terms <> App constr
R8082:8095 SF_reduction <> left_component def
R8075:8079 Equal <> equal def
R8034:8047 LamSF_Tactics <> transitive_red thm
R8211:8225 Equal <> equal_compounds thm
R8258:8267 LamSF_Tactics <> multi_step ind
R8281:8283 LamSF_Terms <> App constr
R8286:8288 LamSF_Terms <> App constr
R8269:8278 LamSF_reduction <> lamSF_red1 ind
R8258:8267 LamSF_Tactics <> multi_step ind
R8281:8283 LamSF_Terms <> App constr
R8286:8288 LamSF_Terms <> App constr
R8269:8278 LamSF_reduction <> lamSF_red1 ind
R8334:8336 LamSF_Terms <> App constr
R8339:8341 LamSF_Terms <> App constr
R8344:8346 LamSF_Terms <> App constr
R8353:8356 SF_reduction <> i_op def
R8348:8351 SF_reduction <> k_op def
R8312:8325 LamSF_Tactics <> transitive_red thm
R8334:8336 LamSF_Terms <> App constr
R8339:8341 LamSF_Terms <> App constr
R8344:8346 LamSF_Terms <> App constr
R8353:8356 SF_reduction <> i_op def
R8348:8351 SF_reduction <> k_op def
R8312:8325 LamSF_Tactics <> transitive_red thm
R8378:8400 LamSF_reduction <> preserves_app_lamSF_red thm
R8412:8434 LamSF_reduction <> preserves_app_lamSF_red thm
R8446:8461 Equal <> unequal_programs thm
R8553:8562 LamSF_Tactics <> multi_step ind
R8576:8578 LamSF_Terms <> App constr
R8581:8583 LamSF_Terms <> App constr
R8564:8573 LamSF_reduction <> lamSF_red1 ind
R8553:8562 LamSF_Tactics <> multi_step ind
R8576:8578 LamSF_Terms <> App constr
R8581:8583 LamSF_Terms <> App constr
R8564:8573 LamSF_reduction <> lamSF_red1 ind
R8629:8631 LamSF_Terms <> App constr
R8634:8636 LamSF_Terms <> App constr
R8639:8641 LamSF_Terms <> App constr
R8648:8651 SF_reduction <> i_op def
R8643:8646 SF_reduction <> k_op def
R8607:8620 LamSF_Tactics <> transitive_red thm
R8629:8631 LamSF_Terms <> App constr
R8634:8636 LamSF_Terms <> App constr
R8639:8641 LamSF_Terms <> App constr
R8648:8651 SF_reduction <> i_op def
R8643:8646 SF_reduction <> k_op def
R8607:8620 LamSF_Tactics <> transitive_red thm
R8673:8695 LamSF_reduction <> preserves_app_lamSF_red thm
R8707:8729 LamSF_reduction <> preserves_app_lamSF_red thm
R8754:8762 LamSF_reduction <> lamSF_red def
R8765:8767 LamSF_Terms <> App constr
R8770:8772 LamSF_Terms <> App constr
R8754:8762 LamSF_reduction <> lamSF_red def
R8765:8767 LamSF_Terms <> App constr
R8770:8772 LamSF_Terms <> App constr
R8818:8820 LamSF_Terms <> App constr
R8944:8946 LamSF_Terms <> App constr
R8953:8956 SF_reduction <> i_op def
R8948:8951 SF_reduction <> k_op def
R8823:8825 LamSF_Terms <> App constr
R8885:8887 LamSF_Terms <> App constr
R8922:8936 SF_reduction <> right_component def
R8890:8892 LamSF_Terms <> App constr
R8901:8915 SF_reduction <> right_component def
R8894:8898 Equal <> equal def
R8828:8830 LamSF_Terms <> App constr
R8864:8877 SF_reduction <> left_component def
R8833:8835 LamSF_Terms <> App constr
R8844:8857 SF_reduction <> left_component def
R8837:8841 Equal <> equal def
R8796:8809 LamSF_Tactics <> transitive_red thm
R8818:8820 LamSF_Terms <> App constr
R8944:8946 LamSF_Terms <> App constr
R8953:8956 SF_reduction <> i_op def
R8948:8951 SF_reduction <> k_op def
R8823:8825 LamSF_Terms <> App constr
R8885:8887 LamSF_Terms <> App constr
R8922:8936 SF_reduction <> right_component def
R8890:8892 LamSF_Terms <> App constr
R8901:8915 SF_reduction <> right_component def
R8894:8898 Equal <> equal def
R8828:8830 LamSF_Terms <> App constr
R8864:8877 SF_reduction <> left_component def
R8833:8835 LamSF_Terms <> App constr
R8844:8857 SF_reduction <> left_component def
R8837:8841 Equal <> equal def
R8796:8809 LamSF_Tactics <> transitive_red thm
R8973:8987 Equal <> equal_compounds thm
R9020:9029 LamSF_Tactics <> multi_step ind
R9043:9045 LamSF_Terms <> App constr
R9048:9050 LamSF_Terms <> App constr
R9031:9040 LamSF_reduction <> lamSF_red1 ind
R9020:9029 LamSF_Tactics <> multi_step ind
R9043:9045 LamSF_Terms <> App constr
R9048:9050 LamSF_Terms <> App constr
R9031:9040 LamSF_reduction <> lamSF_red1 ind
R9096:9098 LamSF_Terms <> App constr
R9101:9103 LamSF_Terms <> App constr
R9106:9108 LamSF_Terms <> App constr
R9115:9118 SF_reduction <> i_op def
R9110:9113 SF_reduction <> k_op def
R9074:9087 LamSF_Tactics <> transitive_red thm
R9096:9098 LamSF_Terms <> App constr
R9101:9103 LamSF_Terms <> App constr
R9106:9108 LamSF_Terms <> App constr
R9115:9118 SF_reduction <> i_op def
R9110:9113 SF_reduction <> k_op def
R9074:9087 LamSF_Tactics <> transitive_red thm
R9140:9162 LamSF_reduction <> preserves_app_lamSF_red thm
R9174:9196 LamSF_reduction <> preserves_app_lamSF_red thm
R9208:9223 Equal <> unequal_programs thm
R9336:9351 LamSF_Closed <> subst_rec_closed thm
R9353:9357 Equal <> equal def
R9336:9351 LamSF_Closed <> subst_rec_closed thm
R9353:9357 Equal <> equal def
R9385:9389 Combinators <> abs_S def
R9399:9407 LamSF_Terms <> subst_rec def
R9415:9423 LamSF_Terms <> subst_rec def
R9415:9423 LamSF_Terms <> subst_rec def
R9463:9471 LamSF_Terms <> subst_rec def
R9479:9487 LamSF_Terms <> subst_rec def
R9479:9487 LamSF_Terms <> subst_rec def
R9515:9537 LamSF_reduction <> preserves_abs_lamSF_red thm
R9548:9556 LamSF_Terms <> subst_rec def
R9564:9572 LamSF_Terms <> subst_rec def
R9564:9572 LamSF_Terms <> subst_rec def
R9599:9607 LamSF_Terms <> subst_rec def
R9615:9623 LamSF_Terms <> subst_rec def
R9615:9623 LamSF_Terms <> subst_rec def
R9650:9658 LamSF_Terms <> subst_rec def
R9666:9674 LamSF_Terms <> subst_rec def
R9666:9674 LamSF_Terms <> subst_rec def
R9701:9709 LamSF_Terms <> subst_rec def
R9717:9725 LamSF_Terms <> subst_rec def
R9717:9725 LamSF_Terms <> subst_rec def
R9752:9760 LamSF_Terms <> subst_rec def
R9768:9776 LamSF_Terms <> subst_rec def
R9768:9776 LamSF_Terms <> subst_rec def
R9804:9821 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9804:9821 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9804:9821 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9804:9821 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9804:9821 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9844:9861 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9844:9861 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9844:9861 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9844:9861 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9844:9861 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9884:9900 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9884:9900 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9884:9900 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9884:9900 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9884:9900 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9923:9935 LamSF_Substitution_term <> lift_rec_null thm
R9923:9935 LamSF_Substitution_term <> lift_rec_null thm
R9923:9935 LamSF_Substitution_term <> lift_rec_null thm
R9955:9972 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9955:9972 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9955:9972 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9955:9972 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9955:9972 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9995:10012 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9995:10012 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9995:10012 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9995:10012 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9995:10012 LamSF_Substitution_term <> subst_rec_lift_rec thm
R10035:10051 LamSF_Substitution_term <> lift_rec_lift_rec thm
R10035:10051 LamSF_Substitution_term <> lift_rec_lift_rec thm
R10035:10051 LamSF_Substitution_term <> lift_rec_lift_rec thm
R10035:10051 LamSF_Substitution_term <> lift_rec_lift_rec thm
R10035:10051 LamSF_Substitution_term <> lift_rec_lift_rec thm
R10082:10104 LamSF_reduction <> preserves_app_lamSF_red thm
R10129:10147 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R10129:10147 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R10129:10147 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R10178:10196 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R10178:10196 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R10178:10196 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
def 10226:10229 <> wait
R10238:10240 LamSF_Terms <> App constr
R10296:10299 SF_reduction <> i_op def
R10243:10245 LamSF_Terms <> App constr
R10253:10255 LamSF_Terms <> App constr
R10282:10284 LamSF_Terms <> App constr
R10291:10291 Unstar <> N var
R10286:10289 SF_reduction <> k_op def
R10258:10260 LamSF_Terms <> App constr
R10268:10270 LamSF_Terms <> App constr
R10277:10277 Unstar <> M var
R10272:10275 SF_reduction <> k_op def
R10262:10265 SF_reduction <> s_op def
R10247:10250 SF_reduction <> s_op def
prf 10310:10318 <> rank_wait
R10349:10351 Coq.Init.Logic <> :type_scope:x_'='_x not
R10334:10337 LamSF_Tactics <> rank def
R10340:10343 Unstar <> wait def
R10347:10347 Unstar <> N var
R10345:10345 Unstar <> M var
R10363:10365 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10354:10356 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10357:10360 LamSF_Tactics <> rank def
R10362:10362 Unstar <> M var
R10366:10369 LamSF_Tactics <> rank def
R10371:10371 Unstar <> N var
R10400:10403 LamSF_Tactics <> rank def
R10411:10414 LamSF_Tactics <> rank def
R10411:10414 LamSF_Tactics <> rank def
def 10453:10455 <> tag
R10465:10467 LamSF_Terms <> App constr
R10494:10496 LamSF_Terms <> App constr
R10514:10514 Unstar <> T var
R10499:10501 LamSF_Terms <> App constr
R10508:10511 SF_reduction <> k_op def
R10503:10506 SF_reduction <> s_op def
R10470:10472 LamSF_Terms <> App constr
R10480:10482 LamSF_Terms <> App constr
R10489:10489 Unstar <> M var
R10484:10487 SF_reduction <> k_op def
R10474:10477 SF_reduction <> s_op def
def 10587:10593 <> abs_tag
R10598:10600 Unstar <> tag def
R10602:10605 SF_reduction <> f_op def
def 10619:10625 <> com_tag
R10630:10632 Unstar <> tag def
R10634:10637 SF_reduction <> s_op def
def 10651:10657 <> app_tag
R10666:10668 Unstar <> tag def
R10676:10679 Unstar <> wait def
R10683:10683 Unstar <> N var
R10681:10681 Unstar <> M var
R10670:10673 SF_reduction <> k_op def
R10714:10720 Unstar <> abs_tag def
R10723:10730 SF_reduction <> abs_left def
R10733:10739 Unstar <> com_tag def
R10742:10748 Unstar <> app_tag def
R10751:10753 Unstar <> tag def
R10756:10759 Unstar <> wait def
R10762:10765 SF_reduction <> i_op def
R10768:10769 Coq.Init.Datatypes <> id def
R10772:10775 SF_reduction <> k_op def
R10778:10781 SF_reduction <> f_op def
R10784:10787 SF_reduction <> s_op def
prf 10797:10804 <> wait_ext
R10820:10830 Eta <> beta_eta_eq ind
R10844:10846 LamSF_Terms <> App constr
R10850:10850 Unstar <> N var
R10848:10848 Unstar <> M var
R10833:10836 Unstar <> wait def
R10840:10840 Unstar <> N var
R10838:10838 Unstar <> M var
R10881:10884 Unstar <> wait def
R10895:10905 Eta <> beta_eta_eq ind
R10973:10975 LamSF_Terms <> Abs constr
R10978:10980 LamSF_Terms <> App constr
R11063:11065 LamSF_Terms <> Ref constr
R10983:10990 LamSF_Terms <> lift_rec def
R10993:10995 LamSF_Terms <> App constr
R11051:11054 SF_reduction <> i_op def
R10998:11000 LamSF_Terms <> App constr
R11008:11010 LamSF_Terms <> App constr
R11037:11039 LamSF_Terms <> App constr
R11041:11044 SF_reduction <> k_op def
R11013:11015 LamSF_Terms <> App constr
R11023:11025 LamSF_Terms <> App constr
R11027:11030 SF_reduction <> k_op def
R11017:11020 SF_reduction <> s_op def
R11002:11005 SF_reduction <> s_op def
R10908:10910 LamSF_Terms <> App constr
R10966:10969 SF_reduction <> i_op def
R10913:10915 LamSF_Terms <> App constr
R10923:10925 LamSF_Terms <> App constr
R10952:10954 LamSF_Terms <> App constr
R10956:10959 SF_reduction <> k_op def
R10928:10930 LamSF_Terms <> App constr
R10938:10940 LamSF_Terms <> App constr
R10942:10945 SF_reduction <> k_op def
R10932:10935 SF_reduction <> s_op def
R10917:10920 SF_reduction <> s_op def
R10895:10905 Eta <> beta_eta_eq ind
R10973:10975 LamSF_Terms <> Abs constr
R10978:10980 LamSF_Terms <> App constr
R11063:11065 LamSF_Terms <> Ref constr
R10983:10990 LamSF_Terms <> lift_rec def
R10993:10995 LamSF_Terms <> App constr
R11051:11054 SF_reduction <> i_op def
R10998:11000 LamSF_Terms <> App constr
R11008:11010 LamSF_Terms <> App constr
R11037:11039 LamSF_Terms <> App constr
R11041:11044 SF_reduction <> k_op def
R11013:11015 LamSF_Terms <> App constr
R11023:11025 LamSF_Terms <> App constr
R11027:11030 SF_reduction <> k_op def
R11017:11020 SF_reduction <> s_op def
R11002:11005 SF_reduction <> s_op def
R10908:10910 LamSF_Terms <> App constr
R10966:10969 SF_reduction <> i_op def
R10913:10915 LamSF_Terms <> App constr
R10923:10925 LamSF_Terms <> App constr
R10952:10954 LamSF_Terms <> App constr
R10956:10959 SF_reduction <> k_op def
R10928:10930 LamSF_Terms <> App constr
R10938:10940 LamSF_Terms <> App constr
R10942:10945 SF_reduction <> k_op def
R10932:10935 SF_reduction <> s_op def
R10917:10920 SF_reduction <> s_op def
R11103:11113 Eta <> beta_eta_eq ind
R11513:11515 LamSF_Terms <> Abs constr
R11518:11520 LamSF_Terms <> App constr
R11563:11565 LamSF_Terms <> Ref constr
R11523:11525 LamSF_Terms <> App constr
R11545:11552 LamSF_Terms <> lift_rec def
R11528:11535 LamSF_Terms <> lift_rec def
R11117:11119 LamSF_Terms <> Abs constr
R11133:11135 LamSF_Terms <> App constr
R11503:11505 LamSF_Terms <> Ref constr
R11152:11154 LamSF_Terms <> App constr
R11413:11415 LamSF_Terms <> App constr
R11477:11479 LamSF_Terms <> App constr
R11491:11492 LamSF_Terms <> Op constr
R11494:11496 LamSF_Terms <> Fop constr
R11482:11483 LamSF_Terms <> Op constr
R11485:11487 LamSF_Terms <> Fop constr
R11418:11420 LamSF_Terms <> App constr
R11432:11434 LamSF_Terms <> App constr
R11446:11447 LamSF_Terms <> Op constr
R11449:11451 LamSF_Terms <> Fop constr
R11437:11438 LamSF_Terms <> Op constr
R11440:11442 LamSF_Terms <> Fop constr
R11423:11424 LamSF_Terms <> Op constr
R11426:11428 LamSF_Terms <> Sop constr
R11174:11176 LamSF_Terms <> App constr
R11208:11210 LamSF_Terms <> App constr
R11347:11349 LamSF_Terms <> App constr
R11376:11383 LamSF_Terms <> lift_rec def
R11352:11354 LamSF_Terms <> App constr
R11366:11367 LamSF_Terms <> Op constr
R11369:11371 LamSF_Terms <> Fop constr
R11357:11358 LamSF_Terms <> Op constr
R11360:11362 LamSF_Terms <> Fop constr
R11236:11238 LamSF_Terms <> App constr
R11276:11278 LamSF_Terms <> App constr
R11305:11312 LamSF_Terms <> lift_rec def
R11281:11283 LamSF_Terms <> App constr
R11295:11296 LamSF_Terms <> Op constr
R11298:11300 LamSF_Terms <> Fop constr
R11286:11287 LamSF_Terms <> Op constr
R11289:11291 LamSF_Terms <> Fop constr
R11241:11242 LamSF_Terms <> Op constr
R11244:11246 LamSF_Terms <> Sop constr
R11179:11180 LamSF_Terms <> Op constr
R11182:11184 LamSF_Terms <> Sop constr
R11103:11113 Eta <> beta_eta_eq ind
R11513:11515 LamSF_Terms <> Abs constr
R11518:11520 LamSF_Terms <> App constr
R11563:11565 LamSF_Terms <> Ref constr
R11523:11525 LamSF_Terms <> App constr
R11545:11552 LamSF_Terms <> lift_rec def
R11528:11535 LamSF_Terms <> lift_rec def
R11117:11119 LamSF_Terms <> Abs constr
R11133:11135 LamSF_Terms <> App constr
R11503:11505 LamSF_Terms <> Ref constr
R11152:11154 LamSF_Terms <> App constr
R11413:11415 LamSF_Terms <> App constr
R11477:11479 LamSF_Terms <> App constr
R11491:11492 LamSF_Terms <> Op constr
R11494:11496 LamSF_Terms <> Fop constr
R11482:11483 LamSF_Terms <> Op constr
R11485:11487 LamSF_Terms <> Fop constr
R11418:11420 LamSF_Terms <> App constr
R11432:11434 LamSF_Terms <> App constr
R11446:11447 LamSF_Terms <> Op constr
R11449:11451 LamSF_Terms <> Fop constr
R11437:11438 LamSF_Terms <> Op constr
R11440:11442 LamSF_Terms <> Fop constr
R11423:11424 LamSF_Terms <> Op constr
R11426:11428 LamSF_Terms <> Sop constr
R11174:11176 LamSF_Terms <> App constr
R11208:11210 LamSF_Terms <> App constr
R11347:11349 LamSF_Terms <> App constr
R11376:11383 LamSF_Terms <> lift_rec def
R11352:11354 LamSF_Terms <> App constr
R11366:11367 LamSF_Terms <> Op constr
R11369:11371 LamSF_Terms <> Fop constr
R11357:11358 LamSF_Terms <> Op constr
R11360:11362 LamSF_Terms <> Fop constr
R11236:11238 LamSF_Terms <> App constr
R11276:11278 LamSF_Terms <> App constr
R11305:11312 LamSF_Terms <> lift_rec def
R11281:11283 LamSF_Terms <> App constr
R11295:11296 LamSF_Terms <> Op constr
R11298:11300 LamSF_Terms <> Fop constr
R11286:11287 LamSF_Terms <> Op constr
R11289:11291 LamSF_Terms <> Fop constr
R11241:11242 LamSF_Terms <> Op constr
R11244:11246 LamSF_Terms <> Sop constr
R11179:11180 LamSF_Terms <> Op constr
R11182:11184 LamSF_Terms <> Sop constr
R11583:11592 Eta <> abs_etared constr
R11602:11612 Eta <> beta_eta_eq ind
R11941:11943 LamSF_Terms <> App constr
R12098:12100 LamSF_Terms <> App constr
R12108:12110 LamSF_Terms <> Ref constr
R12102:12105 SF_reduction <> i_op def
R11947:11949 LamSF_Terms <> App constr
R12081:12083 LamSF_Terms <> Ref constr
R11952:11954 LamSF_Terms <> App constr
R12033:12035 LamSF_Terms <> App constr
R12062:12069 LamSF_Terms <> lift_rec def
R12038:12040 LamSF_Terms <> App constr
R12052:12053 LamSF_Terms <> Op constr
R12055:12057 LamSF_Terms <> Fop constr
R12043:12044 LamSF_Terms <> Op constr
R12046:12048 LamSF_Terms <> Fop constr
R11957:11959 LamSF_Terms <> App constr
R11971:11973 LamSF_Terms <> App constr
R12000:12007 LamSF_Terms <> lift_rec def
R11976:11978 LamSF_Terms <> App constr
R11990:11991 LamSF_Terms <> Op constr
R11993:11995 LamSF_Terms <> Fop constr
R11981:11982 LamSF_Terms <> Op constr
R11984:11986 LamSF_Terms <> Fop constr
R11962:11963 LamSF_Terms <> Op constr
R11965:11967 LamSF_Terms <> Sop constr
R11619:11621 LamSF_Terms <> App constr
R11921:11923 LamSF_Terms <> Ref constr
R11632:11634 LamSF_Terms <> App constr
R11837:11839 LamSF_Terms <> App constr
R11895:11897 LamSF_Terms <> App constr
R11909:11910 LamSF_Terms <> Op constr
R11912:11914 LamSF_Terms <> Fop constr
R11900:11901 LamSF_Terms <> Op constr
R11903:11905 LamSF_Terms <> Fop constr
R11842:11844 LamSF_Terms <> App constr
R11856:11858 LamSF_Terms <> App constr
R11870:11871 LamSF_Terms <> Op constr
R11873:11875 LamSF_Terms <> Fop constr
R11861:11862 LamSF_Terms <> Op constr
R11864:11866 LamSF_Terms <> Fop constr
R11847:11848 LamSF_Terms <> Op constr
R11850:11852 LamSF_Terms <> Sop constr
R11648:11650 LamSF_Terms <> App constr
R11676:11678 LamSF_Terms <> App constr
R11777:11779 LamSF_Terms <> App constr
R11806:11813 LamSF_Terms <> lift_rec def
R11782:11784 LamSF_Terms <> App constr
R11796:11797 LamSF_Terms <> Op constr
R11799:11801 LamSF_Terms <> Fop constr
R11787:11788 LamSF_Terms <> Op constr
R11790:11792 LamSF_Terms <> Fop constr
R11698:11700 LamSF_Terms <> App constr
R11712:11714 LamSF_Terms <> App constr
R11741:11748 LamSF_Terms <> lift_rec def
R11717:11719 LamSF_Terms <> App constr
R11731:11732 LamSF_Terms <> Op constr
R11734:11736 LamSF_Terms <> Fop constr
R11722:11723 LamSF_Terms <> Op constr
R11725:11727 LamSF_Terms <> Fop constr
R11703:11704 LamSF_Terms <> Op constr
R11706:11708 LamSF_Terms <> Sop constr
R11653:11654 LamSF_Terms <> Op constr
R11656:11658 LamSF_Terms <> Sop constr
R11602:11612 Eta <> beta_eta_eq ind
R11941:11943 LamSF_Terms <> App constr
R12098:12100 LamSF_Terms <> App constr
R12108:12110 LamSF_Terms <> Ref constr