forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
SF_reduction.glob
1798 lines (1798 loc) · 74.9 KB
/
SF_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
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 9c1127e37c6fddedbdb5227e91cef52a
FSF_reduction
R2136:2140 Coq.Arith.Arith <> <> lib
R2158:2161 Test <> <> lib
R2180:2186 General <> <> lib
R2204:2214 LamSF_Terms <> <> lib
R2233:2245 LamSF_Tactics <> <> lib
R2263:2285 LamSF_Substitution_term <> <> lib
R2304:2317 Beta_Reduction <> <> lib
R2335:2350 LamSF_Confluence <> <> lib
R2369:2373 Coq.omega.Omega <> <> lib
def 2389:2392 <> s_op
R2397:2398 LamSF_Terms <> Op constr
R2400:2402 LamSF_Terms <> Sop constr
def 2416:2419 <> f_op
R2424:2425 LamSF_Terms <> Op constr
R2427:2429 LamSF_Terms <> Fop constr
def 2443:2446 <> k_op
R2451:2453 LamSF_Terms <> App constr
R2460:2463 SF_reduction <> f_op def
R2455:2458 SF_reduction <> f_op def
def 2478:2481 <> i_op
R2486:2488 LamSF_Terms <> App constr
R2506:2509 SF_reduction <> k_op def
R2491:2493 LamSF_Terms <> App constr
R2500:2503 SF_reduction <> k_op def
R2495:2498 SF_reduction <> s_op def
def 2523:2530 <> abs_left
R2535:2537 LamSF_Terms <> App constr
R2555:2558 SF_reduction <> f_op def
R2540:2542 LamSF_Terms <> App constr
R2549:2552 SF_reduction <> k_op def
R2544:2547 SF_reduction <> s_op def
R2586:2593 SF_reduction <> abs_left def
R2596:2599 SF_reduction <> i_op def
R2602:2603 Coq.Init.Datatypes <> id def
R2606:2609 SF_reduction <> k_op def
R2612:2615 SF_reduction <> f_op def
R2618:2621 SF_reduction <> s_op def
def 2657:2660 <> star
R2674:2674 SF_reduction <> M var
R2684:2686 LamSF_Terms <> Ref constr
R2693:2696 SF_reduction <> i_op def
R2701:2703 LamSF_Terms <> Ref constr
R2706:2706 Coq.Init.Datatypes <> S constr
R2714:2716 LamSF_Terms <> App constr
R2724:2726 LamSF_Terms <> Ref constr
R2718:2721 SF_reduction <> k_op def
R2733:2734 LamSF_Terms <> Op constr
R2741:2743 LamSF_Terms <> App constr
R2751:2752 LamSF_Terms <> Op constr
R2745:2748 SF_reduction <> k_op def
R2759:2761 LamSF_Terms <> Abs constr
R2770:2772 LamSF_Terms <> Abs constr
R2775:2778 SF_reduction <> star def
R2786:2788 LamSF_Terms <> App constr
R2799:2801 LamSF_Terms <> App constr
R2824:2826 LamSF_Terms <> Abs constr
R2804:2806 LamSF_Terms <> App constr
R2814:2816 LamSF_Terms <> Abs constr
R2808:2811 SF_reduction <> s_op def
prf 2847:2855 <> rank_star
R2882:2884 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R2869:2872 LamSF_Tactics <> rank def
R2875:2878 SF_reduction <> star def
R2880:2880 SF_reduction <> M var
R2885:2888 LamSF_Tactics <> rank def
R2891:2893 LamSF_Terms <> Abs constr
R2895:2895 SF_reduction <> M var
R3009:3012 SF_reduction <> star def
R3015:3018 LamSF_Tactics <> rank def
R3026:3029 LamSF_Tactics <> rank def
R3037:3040 SF_reduction <> star def
R3026:3029 LamSF_Tactics <> rank def
R3037:3040 SF_reduction <> star def
R3052:3067 General <> times_monotonic2 thm
R3078:3085 LamSF_Tactics <> abs_rank def
R3104:3116 LamSF_Tactics <> rank_positive thm
R3136:3139 SF_reduction <> star def
R3147:3150 SF_reduction <> star def
R3147:3150 SF_reduction <> star def
R3172:3175 LamSF_Tactics <> rank def
R3183:3186 LamSF_Tactics <> rank def
R3183:3186 LamSF_Tactics <> rank def
R3206:3208 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3198:3205 LamSF_Tactics <> abs_rank def
R3209:3209 Coq.Init.Datatypes <> S constr
R3219:3221 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3212:3215 LamSF_Tactics <> rank def
R3222:3225 LamSF_Tactics <> rank def
R3269:3271 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3246:3248 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3238:3245 LamSF_Tactics <> abs_rank def
R3257:3260 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3268:3268 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3249:3256 LamSF_Tactics <> abs_rank def
R3261:3264 LamSF_Tactics <> rank def
R3280:3283 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3291:3291 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3272:3279 LamSF_Tactics <> abs_rank def
R3284:3287 LamSF_Tactics <> rank def
R3206:3208 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3198:3205 LamSF_Tactics <> abs_rank def
R3209:3209 Coq.Init.Datatypes <> S constr
R3219:3221 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3212:3215 LamSF_Tactics <> rank def
R3222:3225 LamSF_Tactics <> rank def
R3269:3271 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3246:3248 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3238:3245 LamSF_Tactics <> abs_rank def
R3257:3260 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3268:3268 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3249:3256 LamSF_Tactics <> abs_rank def
R3261:3264 LamSF_Tactics <> rank def
R3280:3283 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3291:3291 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3272:3279 LamSF_Tactics <> abs_rank def
R3284:3287 LamSF_Tactics <> rank def
R3326:3328 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3329:3336 LamSF_Tactics <> abs_rank def
R3350:3357 LamSF_Tactics <> abs_rank def
R3326:3328 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3329:3336 LamSF_Tactics <> abs_rank def
prf 3391:3404 <> star_monotonic
R3436:3439 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3441:3443 Coq.Init.Logic <> :type_scope:x_'='_x not
R3440:3440 SF_reduction <> M var
R3444:3444 SF_reduction <> N var
R3427:3429 Coq.Init.Logic <> :type_scope:x_'='_x not
R3421:3424 SF_reduction <> star def
R3426:3426 SF_reduction <> M var
R3430:3433 SF_reduction <> star def
R3435:3435 SF_reduction <> N var
R3768:3770 Coq.Init.Logic <> :type_scope:x_'='_x not
R3768:3770 Coq.Init.Logic <> :type_scope:x_'='_x not
def 3871:3885 <> right_component
R3892:3896 LamSF_Terms <> lamSF ind
R3909:3909 SF_reduction <> M var
R3919:3921 LamSF_Terms <> App constr
R3936:3938 LamSF_Terms <> Abs constr
R3946:3949 SF_reduction <> star def
R3961:3961 SF_reduction <> M var
def 3980:3993 <> left_component
R4000:4004 LamSF_Terms <> lamSF ind
R4017:4017 SF_reduction <> U var
R4027:4029 LamSF_Terms <> App constr
R4050:4057 SF_reduction <> abs_left def
prf 4073:4092 <> rank_component_app_l
R4139:4141 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4108:4111 LamSF_Tactics <> rank def
R4114:4127 SF_reduction <> left_component def
R4130:4132 LamSF_Terms <> App constr
R4136:4136 SF_reduction <> N var
R4134:4134 SF_reduction <> M var
R4142:4145 LamSF_Tactics <> rank def
R4148:4150 LamSF_Terms <> App constr
R4154:4154 SF_reduction <> N var
R4152:4152 SF_reduction <> M var
prf 4197:4216 <> rank_component_app_r
R4264:4266 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4232:4235 LamSF_Tactics <> rank def
R4238:4252 SF_reduction <> right_component def
R4255:4257 LamSF_Terms <> App constr
R4261:4261 SF_reduction <> N var
R4259:4259 SF_reduction <> M var
R4267:4270 LamSF_Tactics <> rank def
R4273:4275 LamSF_Terms <> App constr
R4279:4279 SF_reduction <> N var
R4277:4277 SF_reduction <> M var
prf 4322:4341 <> rank_component_abs_l
R4384:4386 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4355:4358 LamSF_Tactics <> rank def
R4361:4374 SF_reduction <> left_component def
R4377:4379 LamSF_Terms <> Abs constr
R4381:4381 SF_reduction <> M var
R4387:4390 LamSF_Tactics <> rank def
R4393:4395 LamSF_Terms <> Abs constr
R4397:4397 SF_reduction <> M var
R4491:4492 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4485:4488 LamSF_Tactics <> rank def
R4491:4492 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4485:4488 LamSF_Tactics <> rank def
R4507:4519 LamSF_Tactics <> rank_positive thm
R4530:4543 SF_reduction <> left_component def
R4564:4567 LamSF_Tactics <> rank def
R4575:4578 LamSF_Tactics <> rank def
R4575:4578 LamSF_Tactics <> rank def
R4599:4602 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4620:4620 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4591:4598 LamSF_Tactics <> abs_rank def
R4611:4613 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4603:4610 LamSF_Tactics <> abs_rank def
R4614:4617 LamSF_Tactics <> rank def
R4648:4650 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4637:4639 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4629:4636 LamSF_Tactics <> abs_rank def
R4640:4647 LamSF_Tactics <> abs_rank def
R4651:4654 LamSF_Tactics <> rank def
R4599:4602 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4620:4620 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4591:4598 LamSF_Tactics <> abs_rank def
R4611:4613 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4603:4610 LamSF_Tactics <> abs_rank def
R4614:4617 LamSF_Tactics <> rank def
R4648:4650 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4637:4639 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4629:4636 LamSF_Tactics <> abs_rank def
R4640:4647 LamSF_Tactics <> abs_rank def
R4651:4654 LamSF_Tactics <> rank def
R4707:4709 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4674:4674 Coq.Init.Datatypes <> S constr
R4694:4696 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4677:4677 Coq.Init.Datatypes <> S constr
R4681:4683 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4684:4684 Coq.Init.Datatypes <> S constr
R4688:4690 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4697:4697 Coq.Init.Datatypes <> S constr
R4701:4703 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4718:4720 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4710:4717 LamSF_Tactics <> abs_rank def
R4721:4728 LamSF_Tactics <> abs_rank def
R4707:4709 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4674:4674 Coq.Init.Datatypes <> S constr
R4694:4696 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4677:4677 Coq.Init.Datatypes <> S constr
R4681:4683 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4684:4684 Coq.Init.Datatypes <> S constr
R4688:4690 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4697:4697 Coq.Init.Datatypes <> S constr
R4701:4703 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4718:4720 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4710:4717 LamSF_Tactics <> abs_rank def
R4721:4728 LamSF_Tactics <> abs_rank def
R4743:4750 LamSF_Tactics <> abs_rank def
R4788:4791 LamSF_Tactics <> rank def
R4803:4805 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4819:4819 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4806:4809 Coq.Init.Peano <> pred syndef
R4812:4815 LamSF_Tactics <> rank def
R4788:4791 LamSF_Tactics <> rank def
R4803:4805 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4819:4819 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4806:4809 Coq.Init.Peano <> pred syndef
R4812:4815 LamSF_Tactics <> rank def
R4860:4863 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4882:4882 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4849:4851 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4841:4848 LamSF_Tactics <> abs_rank def
R4852:4859 LamSF_Tactics <> abs_rank def
R4865:4867 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4881:4881 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4868:4871 Coq.Init.Peano <> pred syndef
R4874:4877 LamSF_Tactics <> rank def
R4910:4912 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4899:4901 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4891:4898 LamSF_Tactics <> abs_rank def
R4902:4909 LamSF_Tactics <> abs_rank def
R4932:4935 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4949:4949 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4921:4923 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4913:4920 LamSF_Tactics <> abs_rank def
R4924:4931 LamSF_Tactics <> abs_rank def
R4936:4939 Coq.Init.Peano <> pred syndef
R4942:4945 LamSF_Tactics <> rank def
R4860:4863 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4882:4882 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4849:4851 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4841:4848 LamSF_Tactics <> abs_rank def
R4852:4859 LamSF_Tactics <> abs_rank def
R4865:4867 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4881:4881 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4868:4871 Coq.Init.Peano <> pred syndef
R4874:4877 LamSF_Tactics <> rank def
R4910:4912 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4899:4901 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4891:4898 LamSF_Tactics <> abs_rank def
R4902:4909 LamSF_Tactics <> abs_rank def
R4932:4935 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4949:4949 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4921:4923 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4913:4920 LamSF_Tactics <> abs_rank def
R4924:4931 LamSF_Tactics <> abs_rank def
R4936:4939 Coq.Init.Peano <> pred syndef
R4942:4945 LamSF_Tactics <> rank def
R4970:4973 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4993:4995 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4982:4984 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4974:4981 LamSF_Tactics <> abs_rank def
R4985:4992 LamSF_Tactics <> abs_rank def
R4996:4999 Coq.Init.Peano <> pred syndef
R5002:5005 LamSF_Tactics <> rank def
R4970:4973 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4993:4995 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4982:4984 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R4974:4981 LamSF_Tactics <> abs_rank def
R4985:4992 LamSF_Tactics <> abs_rank def
R4996:4999 Coq.Init.Peano <> pred syndef
R5002:5005 LamSF_Tactics <> rank def
R5038:5040 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5027:5029 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5019:5026 LamSF_Tactics <> abs_rank def
R5030:5037 LamSF_Tactics <> abs_rank def
R5041:5044 Coq.Init.Peano <> pred syndef
R5047:5050 LamSF_Tactics <> rank def
R5038:5040 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5027:5029 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5019:5026 LamSF_Tactics <> abs_rank def
R5030:5037 LamSF_Tactics <> abs_rank def
R5041:5044 Coq.Init.Peano <> pred syndef
R5047:5050 LamSF_Tactics <> rank def
R5101:5114 SF_reduction <> left_component def
R5135:5138 LamSF_Tactics <> rank def
R5146:5149 LamSF_Tactics <> rank def
R5146:5149 LamSF_Tactics <> rank def
R5193:5195 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5160:5160 Coq.Init.Datatypes <> S constr
R5180:5182 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5163:5163 Coq.Init.Datatypes <> S constr
R5167:5169 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5170:5170 Coq.Init.Datatypes <> S constr
R5174:5176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5183:5183 Coq.Init.Datatypes <> S constr
R5187:5189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5196:5203 LamSF_Tactics <> abs_rank def
R5193:5195 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5160:5160 Coq.Init.Datatypes <> S constr
R5180:5182 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5163:5163 Coq.Init.Datatypes <> S constr
R5167:5169 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5170:5170 Coq.Init.Datatypes <> S constr
R5174:5176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5183:5183 Coq.Init.Datatypes <> S constr
R5187:5189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5196:5203 LamSF_Tactics <> abs_rank def
R5215:5222 LamSF_Tactics <> abs_rank def
prf 5278:5297 <> rank_component_abs_r
R5341:5343 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5311:5314 LamSF_Tactics <> rank def
R5317:5331 SF_reduction <> right_component def
R5334:5336 LamSF_Terms <> Abs constr
R5338:5338 SF_reduction <> M var
R5344:5347 LamSF_Tactics <> rank def
R5350:5352 LamSF_Terms <> Abs constr
R5354:5354 SF_reduction <> M var
R5374:5388 SF_reduction <> right_component def
R5408:5416 SF_reduction <> rank_star thm
prf 5434:5456 <> lift_rec_preserves_star
R5472:5476 LamSF_Terms <> lamSF ind
R5507:5509 Coq.Init.Logic <> :type_scope:x_'='_x not
R5487:5494 LamSF_Terms <> lift_rec def
R5506:5506 SF_reduction <> k var
R5504:5504 SF_reduction <> n var
R5496:5499 SF_reduction <> star def
R5501:5501 SF_reduction <> M var
R5510:5513 SF_reduction <> star def
R5516:5523 LamSF_Terms <> lift_rec def
R5533:5533 SF_reduction <> k var
R5528:5528 Coq.Init.Datatypes <> S constr
R5530:5530 SF_reduction <> n var
R5525:5525 SF_reduction <> M var
R5599:5611 LamSF_Tactics <> relocate_succ thm
R5599:5611 LamSF_Tactics <> relocate_succ thm
R5599:5611 LamSF_Tactics <> relocate_succ thm
prf 5635:5665 <> lift_rec_preserves_components_l
R5681:5685 LamSF_Terms <> lamSF ind
R5726:5728 Coq.Init.Logic <> :type_scope:x_'='_x not
R5696:5703 LamSF_Terms <> lift_rec def
R5725:5725 SF_reduction <> k var
R5723:5723 SF_reduction <> n var
R5705:5718 SF_reduction <> left_component def
R5720:5720 SF_reduction <> M var
R5729:5742 SF_reduction <> left_component def
R5744:5751 LamSF_Terms <> lift_rec def
R5757:5757 SF_reduction <> k var
R5755:5755 SF_reduction <> n var
R5753:5753 SF_reduction <> M var
prf 5834:5864 <> lift_rec_preserves_components_r
R5880:5884 LamSF_Terms <> lamSF ind
R5926:5928 Coq.Init.Logic <> :type_scope:x_'='_x not
R5895:5902 LamSF_Terms <> lift_rec def
R5925:5925 SF_reduction <> k var
R5923:5923 SF_reduction <> n var
R5904:5918 SF_reduction <> right_component def
R5920:5920 SF_reduction <> M var
R5929:5943 SF_reduction <> right_component def
R5945:5952 LamSF_Terms <> lift_rec def
R5958:5958 SF_reduction <> k var
R5956:5956 SF_reduction <> n var
R5954:5954 SF_reduction <> M var
R6002:6024 SF_reduction <> lift_rec_preserves_star thm
R6002:6024 SF_reduction <> lift_rec_preserves_star thm
R6002:6024 SF_reduction <> lift_rec_preserves_star thm
prf 6050:6070 <> star_preserves_status
R6118:6121 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R6101:6103 Coq.Init.Logic <> :type_scope:x_'='_x not
R6086:6091 LamSF_Tactics <> status def
R6094:6097 SF_reduction <> star def
R6099:6099 SF_reduction <> M var
R6104:6107 Coq.Init.Peano <> pred syndef
R6109:6114 LamSF_Tactics <> status def
R6116:6116 SF_reduction <> M var
R6136:6138 Coq.Init.Logic <> :type_scope:x_'='_x not
R6122:6127 LamSF_Tactics <> status def
R6129:6132 SF_reduction <> star def
R6134:6134 SF_reduction <> M var
ind 6276:6283 <> compound
constr 6307:6318 <> op1_compound
constr 6360:6371 <> op2_compound
constr 6423:6437 <> abs_op_compound
constr 6475:6495 <> abs_compound_compound
constr 6542:6560 <> abs_active_compound
R6292:6295 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6287:6291 LamSF_Terms <> lamSF ind
R6334:6341 SF_reduction <> compound ind
R6344:6346 LamSF_Terms <> App constr
R6355:6355 SF_reduction <> M var
R6349:6350 LamSF_Terms <> Op constr
R6352:6352 SF_reduction <> o var
R6389:6396 SF_reduction <> compound ind
R6399:6401 LamSF_Terms <> App constr
R6418:6418 SF_reduction <> N var
R6404:6406 LamSF_Terms <> App constr
R6415:6415 SF_reduction <> M var
R6409:6410 LamSF_Terms <> Op constr
R6412:6412 SF_reduction <> o var
R6451:6458 SF_reduction <> compound ind
R6461:6463 LamSF_Terms <> Abs constr
R6466:6467 LamSF_Terms <> Op constr
R6469:6469 SF_reduction <> o var
R6519:6522 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6523:6530 SF_reduction <> compound ind
R6533:6535 LamSF_Terms <> Abs constr
R6537:6537 SF_reduction <> M var
R6509:6516 SF_reduction <> compound ind
R6518:6518 SF_reduction <> M var
R6585:6588 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6589:6596 SF_reduction <> compound ind
R6599:6601 LamSF_Terms <> Abs constr
R6603:6603 SF_reduction <> M var
R6581:6583 Coq.Init.Logic <> :type_scope:x_'='_x not
R6573:6578 LamSF_Tactics <> status def
R6580:6580 SF_reduction <> M var
prf 6717:6731 <> rank_compound_l
R6755:6759 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6783:6785 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6760:6763 LamSF_Tactics <> rank def
R6766:6779 SF_reduction <> left_component def
R6781:6781 SF_reduction <> M var
R6786:6789 LamSF_Tactics <> rank def
R6791:6791 SF_reduction <> M var
R6745:6752 SF_reduction <> compound ind
R6754:6754 SF_reduction <> M var
R6844:6863 SF_reduction <> rank_component_app_l thm
R6844:6863 SF_reduction <> rank_component_app_l thm
R6844:6863 SF_reduction <> rank_component_app_l thm
R6877:6896 SF_reduction <> rank_component_abs_l thm
R6844:6863 SF_reduction <> rank_component_app_l thm
R6877:6896 SF_reduction <> rank_component_abs_l thm
R6844:6863 SF_reduction <> rank_component_app_l thm
R6877:6896 SF_reduction <> rank_component_abs_l thm
prf 6927:6941 <> rank_compound_r
R6965:6969 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6994:6996 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6970:6973 LamSF_Tactics <> rank def
R6976:6990 SF_reduction <> right_component def
R6992:6992 SF_reduction <> M var
R6997:7000 LamSF_Tactics <> rank def
R7002:7002 SF_reduction <> M var
R6955:6962 SF_reduction <> compound ind
R6964:6964 SF_reduction <> M var
R7055:7074 SF_reduction <> rank_component_app_r thm
R7055:7074 SF_reduction <> rank_component_app_r thm
R7055:7074 SF_reduction <> rank_component_app_r thm
R7088:7107 SF_reduction <> rank_component_abs_r thm
R7055:7074 SF_reduction <> rank_component_app_r thm
R7088:7107 SF_reduction <> rank_component_abs_r thm
R7055:7074 SF_reduction <> rank_component_app_r thm
R7088:7107 SF_reduction <> rank_component_abs_r thm
prf 7141:7167 <> lift_rec_preserves_compound
R7183:7187 LamSF_Terms <> lamSF ind
R7201:7204 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7219:7221 Coq.Init.Datatypes <> nat ind
R7225:7232 SF_reduction <> compound ind
R7234:7241 LamSF_Terms <> lift_rec def
R7247:7247 SF_reduction <> k var
R7245:7245 SF_reduction <> n var
R7243:7243 SF_reduction <> M var
R7191:7198 SF_reduction <> compound ind
R7200:7200 SF_reduction <> M var
R7304:7322 SF_reduction <> abs_active_compound constr
R7360:7362 Coq.Init.Logic <> :type_scope:x_'='_x not
R7333:7338 LamSF_Tactics <> status def
R7341:7348 LamSF_Terms <> lift_rec def
R7353:7353 Coq.Init.Datatypes <> S constr
R7363:7370 LamSF_Terms <> relocate def
R7384:7384 Coq.Init.Datatypes <> S constr
R7387:7387 Coq.Init.Datatypes <> S constr
R7373:7378 LamSF_Tactics <> status def
R7360:7362 Coq.Init.Logic <> :type_scope:x_'='_x not
R7333:7338 LamSF_Tactics <> status def
R7341:7348 LamSF_Terms <> lift_rec def
R7353:7353 Coq.Init.Datatypes <> S constr
R7363:7370 LamSF_Terms <> relocate def
R7384:7384 Coq.Init.Datatypes <> S constr
R7387:7387 Coq.Init.Datatypes <> S constr
R7373:7378 LamSF_Tactics <> status def
R7406:7430 LamSF_Tactics <> lift_rec_preserves_status thm
prf 7532:7559 <> subst_rec_preserves_compound
R7574:7578 LamSF_Terms <> lamSF ind
R7592:7595 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7610:7612 Coq.Init.Datatypes <> nat ind
R7616:7623 SF_reduction <> compound ind
R7625:7633 LamSF_Terms <> subst_rec def
R7639:7639 SF_reduction <> k var
R7637:7637 SF_reduction <> N var
R7635:7635 SF_reduction <> M var
R7582:7589 SF_reduction <> compound ind
R7591:7591 SF_reduction <> M var
R7696:7714 SF_reduction <> abs_active_compound constr
R7753:7755 Coq.Init.Logic <> :type_scope:x_'='_x not
R7725:7730 LamSF_Tactics <> status def
R7733:7741 LamSF_Terms <> subst_rec def
R7748:7748 Coq.Init.Datatypes <> S constr
R7756:7761 LamSF_Tactics <> status def
R7753:7755 Coq.Init.Logic <> :type_scope:x_'='_x not
R7725:7730 LamSF_Tactics <> status def
R7733:7741 LamSF_Terms <> subst_rec def
R7748:7748 Coq.Init.Datatypes <> S constr
R7756:7761 LamSF_Tactics <> status def
R7775:7800 LamSF_Tactics <> subst_rec_preserves_status thm
prf 7885:7903 <> compound_not_active
R7927:7930 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7939:7941 Coq.Init.Logic <> :type_scope:x_'='_x not
R7931:7936 LamSF_Tactics <> status def
R7938:7938 SF_reduction <> M var
R7917:7924 SF_reduction <> compound ind
R7926:7926 SF_reduction <> M var
prf 8009:8021 <> star_compound
R8035:8042 SF_reduction <> compound ind
R8045:8048 SF_reduction <> star def
R8050:8050 SF_reduction <> M var
prf 8156:8186 <> subst_rec_preserves_star_active
R8203:8207 LamSF_Terms <> lamSF ind
R8232:8238 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8260:8262 Coq.Init.Logic <> :type_scope:x_'='_x not
R8239:8247 LamSF_Terms <> subst_rec def
R8259:8259 SF_reduction <> k var
R8257:8257 SF_reduction <> N var
R8249:8252 SF_reduction <> star def
R8254:8254 SF_reduction <> M var
R8263:8266 SF_reduction <> star def
R8269:8277 LamSF_Terms <> subst_rec def
R8284:8284 Coq.Init.Datatypes <> S constr
R8286:8286 SF_reduction <> k var
R8281:8281 SF_reduction <> N var
R8279:8279 SF_reduction <> M var
R8223:8227 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8231:8231 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8215:8220 LamSF_Tactics <> status def
R8222:8222 SF_reduction <> M var
R8228:8228 Coq.Init.Datatypes <> S constr
R8230:8230 SF_reduction <> k var
R8346:8355 LamSF_Terms <> insert_Ref def
R8363:8369 Test <> compare def
R8383:8389 Test <> compare def
R8398:8398 Coq.Init.Datatypes <> S constr
R8392:8392 Coq.Init.Datatypes <> S constr
R8363:8369 Test <> compare def
R8383:8389 Test <> compare def
R8398:8398 Coq.Init.Datatypes <> S constr
R8392:8392 Coq.Init.Datatypes <> S constr
R8383:8389 Test <> compare def
R8398:8398 Coq.Init.Datatypes <> S constr
R8392:8392 Coq.Init.Datatypes <> S constr
prf 8570:8602 <> subst_rec_preserves_star_compound
R8619:8623 LamSF_Terms <> lamSF ind
R8641:8647 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8669:8671 Coq.Init.Logic <> :type_scope:x_'='_x not
R8648:8656 LamSF_Terms <> subst_rec def
R8668:8668 SF_reduction <> k var
R8666:8666 SF_reduction <> N var
R8658:8661 SF_reduction <> star def
R8663:8663 SF_reduction <> M var
R8672:8675 SF_reduction <> star def
R8677:8685 LamSF_Terms <> subst_rec def
R8692:8692 Coq.Init.Datatypes <> S constr
R8694:8694 SF_reduction <> k var
R8689:8689 SF_reduction <> N var
R8687:8687 SF_reduction <> M var
R8631:8638 SF_reduction <> compound ind
R8640:8640 SF_reduction <> M var
R8783:8813 SF_reduction <> subst_rec_preserves_star_active thm
R8783:8813 SF_reduction <> subst_rec_preserves_star_active thm
R8783:8813 SF_reduction <> subst_rec_preserves_star_active thm
R8783:8813 SF_reduction <> subst_rec_preserves_star_active thm
prf 8845:8876 <> subst_rec_preserves_components_l
R8892:8896 LamSF_Terms <> lamSF ind
R8914:8920 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8952:8954 Coq.Init.Logic <> :type_scope:x_'='_x not
R8921:8929 LamSF_Terms <> subst_rec def
R8951:8951 SF_reduction <> k var
R8949:8949 SF_reduction <> n var
R8931:8944 SF_reduction <> left_component def
R8946:8946 SF_reduction <> M var
R8955:8968 SF_reduction <> left_component def
R8970:8978 LamSF_Terms <> subst_rec def
R8984:8984 SF_reduction <> k var
R8982:8982 SF_reduction <> n var
R8980:8980 SF_reduction <> M var
R8904:8911 SF_reduction <> compound ind
R8913:8913 SF_reduction <> M var
R9024:9031 SF_reduction <> compound ind
prf 9049:9087 <> subst_rec_preserves_components_active_r
R9104:9108 LamSF_Terms <> lamSF ind
R9125:9128 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9155:9160 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9193:9195 Coq.Init.Logic <> :type_scope:x_'='_x not
R9161:9169 LamSF_Terms <> subst_rec def
R9192:9192 SF_reduction <> k var
R9190:9190 SF_reduction <> n var
R9171:9185 SF_reduction <> right_component def
R9187:9187 SF_reduction <> M var
R9196:9210 SF_reduction <> right_component def
R9212:9220 LamSF_Terms <> subst_rec def
R9226:9226 SF_reduction <> k var
R9224:9224 SF_reduction <> n var
R9222:9222 SF_reduction <> M var
R9150:9153 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R9142:9147 LamSF_Tactics <> status def
R9149:9149 SF_reduction <> M var
R9154:9154 SF_reduction <> k var
R9121:9123 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R9113:9118 LamSF_Tactics <> status def
R9120:9120 SF_reduction <> M var
R9308:9338 SF_reduction <> subst_rec_preserves_star_active thm
R9308:9338 SF_reduction <> subst_rec_preserves_star_active thm
R9308:9338 SF_reduction <> subst_rec_preserves_star_active thm
R9308:9338 SF_reduction <> subst_rec_preserves_star_active thm
prf 9371:9411 <> subst_rec_preserves_components_compound_r
R9428:9432 LamSF_Terms <> lamSF ind
R9447:9450 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9498:9500 Coq.Init.Logic <> :type_scope:x_'='_x not
R9466:9474 LamSF_Terms <> subst_rec def
R9497:9497 SF_reduction <> k var
R9495:9495 SF_reduction <> n var
R9476:9490 SF_reduction <> right_component def
R9492:9492 SF_reduction <> M var
R9501:9515 SF_reduction <> right_component def
R9517:9525 LamSF_Terms <> subst_rec def
R9531:9531 SF_reduction <> k var
R9529:9529 SF_reduction <> n var
R9527:9527 SF_reduction <> M var
R9437:9444 SF_reduction <> compound ind
R9446:9446 SF_reduction <> M var
R9606:9638 SF_reduction <> subst_rec_preserves_star_compound thm
R9606:9638 SF_reduction <> subst_rec_preserves_star_compound thm
R9606:9638 SF_reduction <> subst_rec_preserves_star_compound thm
R9606:9638 SF_reduction <> subst_rec_preserves_star_compound thm
R9664:9694 SF_reduction <> subst_rec_preserves_star_active thm
R9664:9694 SF_reduction <> subst_rec_preserves_star_active thm
R9664:9694 SF_reduction <> subst_rec_preserves_star_active thm
R9664:9694 SF_reduction <> subst_rec_preserves_star_active thm
def 9731:9748 <> preserves_compound
R9755:9761 LamSF_Tactics <> termred def
R9788:9791 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9809:9813 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9824:9827 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9814:9821 SF_reduction <> compound ind
R9823:9823 SF_reduction <> N var
R9869:9872 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9828:9830 SF_reduction <> red var
R9852:9865 SF_reduction <> left_component def
R9867:9867 SF_reduction <> N var
R9833:9846 SF_reduction <> left_component def
R9848:9848 SF_reduction <> M var
R9873:9875 SF_reduction <> red var
R9897:9911 SF_reduction <> right_component def
R9913:9913 SF_reduction <> N var
R9877:9891 SF_reduction <> right_component def
R9893:9893 SF_reduction <> M var
R9802:9804 SF_reduction <> red var
R9808:9808 SF_reduction <> N var
R9806:9806 SF_reduction <> M var
R9778:9785 SF_reduction <> compound ind
R9787:9787 SF_reduction <> M var
prf 9925:9946 <> preserves_compound_seq
R9969:9975 LamSF_Tactics <> termred def
R10002:10005 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10029:10061 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10062:10079 SF_reduction <> preserves_compound def
R10082:10091 LamSF_Tactics <> sequential ind
R10098:10101 SF_reduction <> red2 var
R10093:10096 SF_reduction <> red1 var
R10006:10023 SF_reduction <> preserves_compound def
R10025:10028 SF_reduction <> red2 var
R9979:9996 SF_reduction <> preserves_compound def
R9998:10001 SF_reduction <> red1 var
R10271:10277 LamSF_Tactics <> seq_red constr
R10363:10369 LamSF_Tactics <> seq_red constr
prf 10387:10415 <> preserves_compound_multi_step
R10432:10438 LamSF_Tactics <> termred def
R10464:10467 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10468:10485 SF_reduction <> preserves_compound def
R10488:10497 LamSF_Tactics <> multi_step ind
R10499:10501 SF_reduction <> red var
R10442:10459 SF_reduction <> preserves_compound def
R10461:10463 SF_reduction <> red var
R10611:10624 SF_reduction <> left_component def
R10596:10603 LamSF_Tactics <> succ_red constr
R10611:10624 SF_reduction <> left_component def
R10596:10603 LamSF_Tactics <> succ_red constr
R10694:10708 SF_reduction <> right_component def
R10679:10686 LamSF_Tactics <> succ_red constr
R10694:10708 SF_reduction <> right_component def
R10679:10686 LamSF_Tactics <> succ_red constr
ind 10848:10853 <> opred1
constr 10872:10880 <> ref_opred
constr 10921:10928 <> op_opred
constr 10967:10975 <> app_opred
constr 11097:11105 <> abs_opred
constr 11166:11170 <> s_red
constr 11404:11411 <> f_op_red
constr 11514:11527 <> f_compound_red
R10857:10863 LamSF_Tactics <> termred def
R10894:10899 SF_reduction <> opred1 ind
R10910:10912 LamSF_Terms <> Ref constr
R10914:10914 SF_reduction <> i var
R10902:10904 LamSF_Terms <> Ref constr
R10906:10906 SF_reduction <> i var
R10942:10947 SF_reduction <> opred1 ind
R10957:10958 LamSF_Terms <> Op constr
R10960:10960 SF_reduction <> o var
R10950:10951 LamSF_Terms <> Op constr
R10953:10953 SF_reduction <> o var
R11016:11025 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11040:11044 LamSF_Terms <> lamSF ind
R11058:11061 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11062:11067 SF_reduction <> opred1 ind
R11080:11082 LamSF_Terms <> App constr
R11087:11088 SF_reduction <> N' var
R11084:11085 SF_reduction <> M' var
R11070:11072 LamSF_Terms <> App constr
R11076:11076 SF_reduction <> N var
R11074:11074 SF_reduction <> M var
R11047:11052 SF_reduction <> opred1 ind
R11056:11057 SF_reduction <> N' var
R11054:11054 SF_reduction <> N var
R11005:11010 SF_reduction <> opred1 ind
R11014:11015 SF_reduction <> M' var
R11012:11012 SF_reduction <> M var
R11134:11137 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11138:11143 SF_reduction <> opred1 ind
R11154:11156 LamSF_Terms <> Abs constr
R11158:11159 SF_reduction <> M' var
R11146:11148 LamSF_Terms <> Abs constr
R11150:11150 SF_reduction <> M var
R11123:11128 SF_reduction <> opred1 ind
R11132:11133 SF_reduction <> M' var
R11130:11130 SF_reduction <> M var
R11198:11202 LamSF_Terms <> lamSF ind
R11230:11233 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11245:11248 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11260:11294 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11295:11300 SF_reduction <> opred1 ind
R11371:11373 LamSF_Terms <> App constr
R11388:11390 LamSF_Terms <> App constr
R11395:11396 SF_reduction <> P' var
R11392:11393 SF_reduction <> N' var
R11376:11378 LamSF_Terms <> App constr
R11383:11384 SF_reduction <> P' var
R11380:11381 SF_reduction <> M' var
R11323:11325 LamSF_Terms <> App constr
R11348:11348 SF_reduction <> P var
R11328:11330 LamSF_Terms <> App constr
R11345:11345 SF_reduction <> N var
R11333:11335 LamSF_Terms <> App constr
R11342:11342 SF_reduction <> M var
R11337:11340 SF_reduction <> s_op def
R11249:11254 SF_reduction <> opred1 ind
R11258:11259 SF_reduction <> P' var
R11256:11256 SF_reduction <> P var
R11234:11239 SF_reduction <> opred1 ind
R11243:11244 SF_reduction <> N' var
R11241:11241 SF_reduction <> N var
R11219:11224 SF_reduction <> opred1 ind
R11228:11229 SF_reduction <> M' var
R11226:11226 SF_reduction <> M var
R11445:11464 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11465:11470 SF_reduction <> opred1 ind
R11506:11507 SF_reduction <> M' var
R11473:11475 LamSF_Terms <> App constr
R11503:11503 SF_reduction <> N var
R11478:11480 LamSF_Terms <> App constr
R11500:11500 SF_reduction <> M var
R11483:11485 LamSF_Terms <> App constr
R11493:11494 LamSF_Terms <> Op constr
R11496:11496 SF_reduction <> o var
R11487:11490 SF_reduction <> f_op def
R11434:11439 SF_reduction <> opred1 ind
R11443:11444 SF_reduction <> M' var
R11441:11441 SF_reduction <> M var
R11551:11555 LamSF_Terms <> lamSF ind
R11569:11586 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11598:11601 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11613:11630 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11631:11636 SF_reduction <> opred1 ind
R11689:11691 LamSF_Terms <> App constr
R11723:11737 SF_reduction <> right_component def
R11739:11740 SF_reduction <> P' var
R11694:11696 LamSF_Terms <> App constr
R11702:11715 SF_reduction <> left_component def
R11717:11718 SF_reduction <> P' var
R11698:11699 SF_reduction <> N' var
R11639:11641 LamSF_Terms <> App constr
R11664:11664 SF_reduction <> N var
R11644:11646 LamSF_Terms <> App constr
R11661:11661 SF_reduction <> M var
R11649:11651 LamSF_Terms <> App constr
R11658:11658 SF_reduction <> P var
R11653:11656 SF_reduction <> f_op def
R11602:11607 SF_reduction <> opred1 ind
R11611:11612 SF_reduction <> N' var
R11609:11609 SF_reduction <> N var
R11587:11592 SF_reduction <> opred1 ind
R11596:11597 SF_reduction <> P' var
R11594:11594 SF_reduction <> P var
R11559:11566 SF_reduction <> compound ind
R11568:11568 SF_reduction <> P var
def 11847:11851 <> opred
R11856:11865 LamSF_Tactics <> multi_step ind
R11867:11872 SF_reduction <> opred1 ind
prf 11883:11899 <> reflective_opred1
R11903:11912 LamSF_Tactics <> reflective def
R11914:11919 SF_reduction <> opred1 ind
prf 12004:12019 <> reflective_opred
R12023:12032 LamSF_Tactics <> reflective def
R12034:12038 SF_reduction <> opred def
R12055:12059 SF_reduction <> opred def
R12070:12084 LamSF_Tactics <> refl_multi_step thm
prf 12134:12152 <> preserves_abs_opred
R12156:12168 LamSF_Tactics <> preserves_abs def
R12170:12174 SF_reduction <> opred def
R12192:12215 LamSF_Tactics <> preserves_abs_multi_step thm
prf 12282:12300 <> preserves_app_opred
R12304:12316 LamSF_Tactics <> preserves_app def
R12318:12322 SF_reduction <> opred def
R12340:12363 LamSF_Tactics <> preserves_app_multi_step thm
prf 12431:12458 <> preserves_star_opred1_active
R12485:12488 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12509:12513 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12514:12519 SF_reduction <> opred1 ind
R12531:12534 SF_reduction <> star def
R12536:12536 SF_reduction <> N var
R12522:12525 SF_reduction <> star def
R12527:12527 SF_reduction <> M var
R12499:12504 SF_reduction <> opred1 ind
R12508:12508 SF_reduction <> N var
R12506:12506 SF_reduction <> M var
R12481:12483 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R12473:12478 LamSF_Tactics <> status def
R12480:12480 SF_reduction <> M var
R12681:12689 SF_reduction <> abs_opred constr
R12784:12786 Coq.Init.Logic <> :type_scope:x_'='_x not
R12776:12781 LamSF_Tactics <> status def
R12784:12786 Coq.Init.Logic <> :type_scope:x_'='_x not
R12776:12781 LamSF_Tactics <> status def
R12801:12819 SF_reduction <> compound_not_active thm
prf 12844:12873 <> preserves_star_opred1_compound
R12898:12901 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12922:12926 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12927:12932 SF_reduction <> opred1 ind
R12944:12947 SF_reduction <> star def
R12949:12949 SF_reduction <> N var
R12935:12938 SF_reduction <> star def
R12940:12940 SF_reduction <> M var
R12912:12917 SF_reduction <> opred1 ind
R12921:12921 SF_reduction <> N var
R12919:12919 SF_reduction <> M var
R12888:12895 SF_reduction <> compound ind
R12897:12897 SF_reduction <> M var
R12991:12998 SF_reduction <> compound ind
R12991:12998 SF_reduction <> compound ind
R12991:12998 SF_reduction <> compound ind
R12991:12998 SF_reduction <> compound ind
R13197:13202 SF_reduction <> opred1 ind
R13214:13217 SF_reduction <> star def
R13205:13208 SF_reduction <> star def
R13197:13202 SF_reduction <> opred1 ind
R13214:13217 SF_reduction <> star def
R13205:13208 SF_reduction <> star def
R13304:13312 SF_reduction <> abs_opred constr
R13323:13350 SF_reduction <> preserves_star_opred1_active thm
prf 13507:13529 <> preserves_status_opred1
R13554:13557 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13578:13581 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13590:13592 Coq.Init.Logic <> :type_scope:x_'='_x not
R13582:13587 LamSF_Tactics <> status def
R13589:13589 SF_reduction <> M var
R13593:13598 LamSF_Tactics <> status def
R13600:13600 SF_reduction <> N var
R13568:13573 SF_reduction <> opred1 ind
R13577:13577 SF_reduction <> N var
R13575:13575 SF_reduction <> M var
R13551:13552 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R13543:13548 LamSF_Tactics <> status def
R13550:13550 SF_reduction <> M var
R13639:13642 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13654:13657 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13678:13681 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13690:13692 Coq.Init.Logic <> :type_scope:x_'='_x not
R13682:13687 LamSF_Tactics <> status def
R13689:13689 SF_reduction <> M var
R13693:13698 LamSF_Tactics <> status def
R13700:13700 SF_reduction <> N var
R13668:13673 SF_reduction <> opred1 ind
R13677:13677 SF_reduction <> N var
R13675:13675 SF_reduction <> M var
R13651:13652 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R13643:13648 LamSF_Tactics <> status def
R13650:13650 SF_reduction <> M var
R13630:13632 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R13629:13629 SF_reduction <> p var
R13633:13636 LamSF_Tactics <> rank def
R13638:13638 SF_reduction <> M var
R13639:13642 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13654:13657 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13678:13681 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13690:13692 Coq.Init.Logic <> :type_scope:x_'='_x not
R13682:13687 LamSF_Tactics <> status def
R13689:13689 SF_reduction <> M var
R13693:13698 LamSF_Tactics <> status def
R13700:13700 SF_reduction <> N var
R13668:13673 SF_reduction <> opred1 ind
R13677:13677 SF_reduction <> N var
R13675:13675 SF_reduction <> M var
R13651:13652 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R13643:13648 LamSF_Tactics <> status def
R13650:13650 SF_reduction <> M var
R13630:13632 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R13629:13629 SF_reduction <> p var
R13633:13636 LamSF_Tactics <> rank def
R13638:13638 SF_reduction <> M var
R13766:13767 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R13760:13763 LamSF_Tactics <> rank def
R13766:13767 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R13760:13763 LamSF_Tactics <> rank def
R13782:13794 LamSF_Tactics <> rank_positive thm
R13929:13931 Coq.Init.Logic <> :type_scope:x_'='_x not
R13921:13926 LamSF_Tactics <> status def
R13932:13937 LamSF_Tactics <> status def
R13929:13931 Coq.Init.Logic <> :type_scope:x_'='_x not
R13921:13926 LamSF_Tactics <> status def
R13932:13937 LamSF_Tactics <> status def
R14664:14666 Coq.Init.Logic <> :type_scope:x_'='_x not
R14655:14660 LamSF_Tactics <> status def
R14664:14666 Coq.Init.Logic <> :type_scope:x_'='_x not
R14655:14660 LamSF_Tactics <> status def
R14681:14699 SF_reduction <> compound_not_active thm
R14789:14791 Coq.Init.Logic <> :type_scope:x_'='_x not
R14744:14749 LamSF_Tactics <> status def
R14752:14754 LamSF_Terms <> App constr
R14757:14759 LamSF_Terms <> App constr
R14762:14764 LamSF_Terms <> App constr
R14767:14769 LamSF_Terms <> App constr
R14792:14797 LamSF_Tactics <> status def
R14801:14803 LamSF_Terms <> App constr
R14806:14808 LamSF_Terms <> App constr
R14811:14813 LamSF_Terms <> App constr
R14789:14791 Coq.Init.Logic <> :type_scope:x_'='_x not
R14744:14749 LamSF_Tactics <> status def
R14752:14754 LamSF_Terms <> App constr
R14757:14759 LamSF_Terms <> App constr
R14762:14764 LamSF_Terms <> App constr
R14767:14769 LamSF_Terms <> App constr
R14792:14797 LamSF_Tactics <> status def
R14801:14803 LamSF_Terms <> App constr
R14806:14808 LamSF_Terms <> App constr
R14811:14813 LamSF_Terms <> App constr
R15126:15128 Coq.Init.Logic <> :type_scope:x_'='_x not
R15077:15082 LamSF_Tactics <> status def
R15085:15087 LamSF_Terms <> App constr
R15090:15092 LamSF_Terms <> App constr
R15095:15097 LamSF_Terms <> App constr
R15100:15102 LamSF_Terms <> App constr
R15129:15134 LamSF_Tactics <> status def
R15138:15140 LamSF_Terms <> App constr
R15143:15145 LamSF_Terms <> App constr
R15148:15150 LamSF_Terms <> App constr
R15126:15128 Coq.Init.Logic <> :type_scope:x_'='_x not
R15077:15082 LamSF_Tactics <> status def
R15085:15087 LamSF_Terms <> App constr
R15090:15092 LamSF_Terms <> App constr
R15095:15097 LamSF_Terms <> App constr
R15100:15102 LamSF_Terms <> App constr
R15129:15134 LamSF_Tactics <> status def
R15138:15140 LamSF_Terms <> App constr
R15143:15145 LamSF_Terms <> App constr
R15148:15150 LamSF_Terms <> App constr
R15420:15422 Coq.Init.Logic <> :type_scope:x_'='_x not
R15412:15417 LamSF_Tactics <> status def