-
Notifications
You must be signed in to change notification settings - Fork 3
/
Extensional_to_combinator.glob
1531 lines (1531 loc) · 68.1 KB
/
Extensional_to_combinator.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 884460f5fdad37a4fd3bb96be8e5bd34
FExtensional_to_combinator
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:2441 Eta <> <> lib
R2459:2463 Coq.omega.Omega <> <> lib
def 2617:2634 <> to_combinator_rank
R2650:2650 Extensional_to_combinator <> p var
R2665:2665 Extensional_to_combinator <> M var
R2670:2670 Coq.Init.Datatypes <> S constr
R2684:2684 Extensional_to_combinator <> M var
R2694:2696 LamSF_Terms <> Ref constr
R2703:2705 LamSF_Terms <> Ref constr
R2712:2713 LamSF_Terms <> Op constr
R2720:2721 LamSF_Terms <> Op constr
R2728:2730 LamSF_Terms <> Abs constr
R2738:2755 Extensional_to_combinator <> to_combinator_rank def
R2760:2763 SF_reduction <> star def
R2771:2773 LamSF_Terms <> App constr
R2784:2786 LamSF_Terms <> App constr
R2815:2832 Extensional_to_combinator <> to_combinator_rank def
R2789:2806 Extensional_to_combinator <> to_combinator_rank def
def 2862:2874 <> to_combinator
R2881:2898 Extensional_to_combinator <> to_combinator_rank def
R2909:2909 Extensional_to_combinator <> M var
R2901:2904 LamSF_Tactics <> rank def
R2906:2906 Extensional_to_combinator <> M var
prf 2922:2946 <> to_combinator_rank_stable
R2969:2972 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2984:2987 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3010:3012 Coq.Init.Logic <> :type_scope:x_'='_x not
R2988:3005 Extensional_to_combinator <> to_combinator_rank def
R3009:3009 Extensional_to_combinator <> M var
R3007:3007 Extensional_to_combinator <> p var
R3013:3030 Extensional_to_combinator <> to_combinator_rank def
R3034:3034 Extensional_to_combinator <> M var
R3032:3032 Extensional_to_combinator <> q var
R2974:2977 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2973:2973 Extensional_to_combinator <> q var
R2978:2981 LamSF_Tactics <> rank def
R2983:2983 Extensional_to_combinator <> M var
R2965:2967 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R2964:2964 Extensional_to_combinator <> p var
R2968:2968 Extensional_to_combinator <> q var
R3084:3085 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3078:3081 LamSF_Tactics <> rank def
R3084:3085 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3078:3081 LamSF_Tactics <> rank def
R3100:3112 LamSF_Tactics <> rank_positive thm
R3156:3158 Coq.Init.Logic <> :type_scope:x_'='_x not
R3159:3159 Coq.Init.Datatypes <> S constr
R3161:3164 Coq.Init.Peano <> pred syndef
R3156:3158 Coq.Init.Logic <> :type_scope:x_'='_x not
R3159:3159 Coq.Init.Datatypes <> S constr
R3161:3164 Coq.Init.Peano <> pred syndef
R3217:3219 Coq.Init.Logic <> :type_scope:x_'='_x not
R3220:3220 Coq.Init.Datatypes <> S constr
R3222:3225 Coq.Init.Peano <> pred syndef
R3217:3219 Coq.Init.Logic <> :type_scope:x_'='_x not
R3220:3220 Coq.Init.Datatypes <> S constr
R3222:3225 Coq.Init.Peano <> pred syndef
R3283:3285 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3277:3280 LamSF_Tactics <> rank def
R3283:3285 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3277:3280 LamSF_Tactics <> rank def
R3300:3312 LamSF_Tactics <> rank_positive thm
R3324:3326 Coq.Init.Logic <> :type_scope:x_'='_x not
R3327:3327 Coq.Init.Datatypes <> S constr
R3329:3332 Coq.Init.Peano <> pred syndef
R3324:3326 Coq.Init.Logic <> :type_scope:x_'='_x not
R3327:3327 Coq.Init.Datatypes <> S constr
R3329:3332 Coq.Init.Peano <> pred syndef
R3409:3411 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3397:3400 LamSF_Tactics <> rank def
R3402:3405 SF_reduction <> star def
R3412:3415 LamSF_Tactics <> rank def
R3418:3420 LamSF_Terms <> Abs constr
R3409:3411 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R3397:3400 LamSF_Tactics <> rank def
R3402:3405 SF_reduction <> star def
R3412:3415 LamSF_Tactics <> rank def
R3418:3420 LamSF_Terms <> Abs constr
R3437:3445 SF_reduction <> rank_star thm
R3487:3489 Coq.Init.Logic <> :type_scope:x_'='_x not
R3490:3490 Coq.Init.Datatypes <> S constr
R3492:3495 Coq.Init.Peano <> pred syndef
R3487:3489 Coq.Init.Logic <> :type_scope:x_'='_x not
R3490:3490 Coq.Init.Datatypes <> S constr
R3492:3495 Coq.Init.Peano <> pred syndef
R3546:3549 Coq.Init.Peano <> pred syndef
R3546:3549 Coq.Init.Peano <> pred syndef
R3546:3549 Coq.Init.Peano <> pred syndef
R3546:3549 Coq.Init.Peano <> pred syndef
R3546:3549 Coq.Init.Peano <> pred syndef
R3584:3587 Coq.Init.Peano <> pred syndef
R3584:3587 Coq.Init.Peano <> pred syndef
R3584:3587 Coq.Init.Peano <> pred syndef
R3584:3587 Coq.Init.Peano <> pred syndef
R3584:3587 Coq.Init.Peano <> pred syndef
prf 3629:3645 <> to_combinator_abs
R3679:3681 Coq.Init.Logic <> :type_scope:x_'='_x not
R3658:3670 Extensional_to_combinator <> to_combinator def
R3673:3675 LamSF_Terms <> Abs constr
R3677:3677 Extensional_to_combinator <> M var
R3682:3694 Extensional_to_combinator <> to_combinator def
R3697:3700 SF_reduction <> star def
R3702:3702 Extensional_to_combinator <> M var
R3734:3746 Extensional_to_combinator <> to_combinator def
R3749:3752 LamSF_Tactics <> rank def
R3755:3772 Extensional_to_combinator <> to_combinator_rank def
R3780:3797 Extensional_to_combinator <> to_combinator_rank def
R3805:3808 LamSF_Tactics <> rank def
R3780:3797 Extensional_to_combinator <> to_combinator_rank def
R3805:3808 LamSF_Tactics <> rank def
R3825:3826 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3819:3822 LamSF_Tactics <> rank def
R3825:3826 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3819:3822 LamSF_Tactics <> rank def
R3841:3853 LamSF_Tactics <> rank_positive thm
R3881:3883 Coq.Init.Logic <> :type_scope:x_'='_x not
R3872:3874 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3864:3871 LamSF_Tactics <> abs_rank def
R3875:3878 LamSF_Tactics <> rank def
R3884:3884 Coq.Init.Datatypes <> S constr
R3887:3890 Coq.Init.Peano <> pred syndef
R3901:3903 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3893:3900 LamSF_Tactics <> abs_rank def
R3904:3907 LamSF_Tactics <> rank def
R3881:3883 Coq.Init.Logic <> :type_scope:x_'='_x not
R3872:3874 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3864:3871 LamSF_Tactics <> abs_rank def
R3875:3878 LamSF_Tactics <> rank def
R3884:3884 Coq.Init.Datatypes <> S constr
R3887:3890 Coq.Init.Peano <> pred syndef
R3901:3903 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R3893:3900 LamSF_Tactics <> abs_rank def
R3904:3907 LamSF_Tactics <> rank def
R3924:3931 LamSF_Tactics <> abs_rank def
R3973:3997 Extensional_to_combinator <> to_combinator_rank_stable thm
R4216:4219 SF_reduction <> star def
R4200:4203 LamSF_Tactics <> rank def
R4206:4209 SF_reduction <> star def
R4000:4003 Coq.Init.Peano <> pred syndef
R4023:4038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4195:4195 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4017:4020 LamSF_Tactics <> rank def
R4045:4061 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4194:4194 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4039:4042 LamSF_Tactics <> rank def
R4068:4085 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4193:4193 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4062:4065 LamSF_Tactics <> rank def
R4092:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4192:4192 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4086:4089 LamSF_Tactics <> rank def
R4117:4136 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4191:4191 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4111:4114 LamSF_Tactics <> rank def
R4143:4146 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4190:4190 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4137:4140 LamSF_Tactics <> rank def
R4153:4156 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4189:4189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4147:4150 LamSF_Tactics <> rank def
R4163:4166 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4188:4188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4157:4160 LamSF_Tactics <> rank def
R4173:4176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4187:4187 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4167:4170 LamSF_Tactics <> rank def
R4183:4185 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4177:4180 LamSF_Tactics <> rank def
R3973:3997 Extensional_to_combinator <> to_combinator_rank_stable thm
R4216:4219 SF_reduction <> star def
R4200:4203 LamSF_Tactics <> rank def
R4206:4209 SF_reduction <> star def
R4000:4003 Coq.Init.Peano <> pred syndef
R4023:4038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4195:4195 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4017:4020 LamSF_Tactics <> rank def
R4045:4061 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4194:4194 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4039:4042 LamSF_Tactics <> rank def
R4068:4085 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4193:4193 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4062:4065 LamSF_Tactics <> rank def
R4092:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4192:4192 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4086:4089 LamSF_Tactics <> rank def
R4117:4136 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4191:4191 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4111:4114 LamSF_Tactics <> rank def
R4143:4146 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4190:4190 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4137:4140 LamSF_Tactics <> rank def
R4153:4156 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4189:4189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4147:4150 LamSF_Tactics <> rank def
R4163:4166 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4188:4188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4157:4160 LamSF_Tactics <> rank def
R4173:4176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4187:4187 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4167:4170 LamSF_Tactics <> rank def
R4183:4185 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4177:4180 LamSF_Tactics <> rank def
R3973:3997 Extensional_to_combinator <> to_combinator_rank_stable thm
R4216:4219 SF_reduction <> star def
R4200:4203 LamSF_Tactics <> rank def
R4206:4209 SF_reduction <> star def
R4000:4003 Coq.Init.Peano <> pred syndef
R4023:4038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4195:4195 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4017:4020 LamSF_Tactics <> rank def
R4045:4061 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4194:4194 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4039:4042 LamSF_Tactics <> rank def
R4068:4085 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4193:4193 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4062:4065 LamSF_Tactics <> rank def
R4092:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4192:4192 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4086:4089 LamSF_Tactics <> rank def
R4117:4136 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4191:4191 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4111:4114 LamSF_Tactics <> rank def
R4143:4146 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4190:4190 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4137:4140 LamSF_Tactics <> rank def
R4153:4156 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4189:4189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4147:4150 LamSF_Tactics <> rank def
R4163:4166 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4188:4188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4157:4160 LamSF_Tactics <> rank def
R4173:4176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4187:4187 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4167:4170 LamSF_Tactics <> rank def
R4183:4185 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4177:4180 LamSF_Tactics <> rank def
R3973:3997 Extensional_to_combinator <> to_combinator_rank_stable thm
R4216:4219 SF_reduction <> star def
R4200:4203 LamSF_Tactics <> rank def
R4206:4209 SF_reduction <> star def
R4000:4003 Coq.Init.Peano <> pred syndef
R4023:4038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4195:4195 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4017:4020 LamSF_Tactics <> rank def
R4045:4061 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4194:4194 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4039:4042 LamSF_Tactics <> rank def
R4068:4085 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4193:4193 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4062:4065 LamSF_Tactics <> rank def
R4092:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4192:4192 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4086:4089 LamSF_Tactics <> rank def
R4117:4136 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4191:4191 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4111:4114 LamSF_Tactics <> rank def
R4143:4146 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4190:4190 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4137:4140 LamSF_Tactics <> rank def
R4153:4156 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4189:4189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4147:4150 LamSF_Tactics <> rank def
R4163:4166 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4188:4188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4157:4160 LamSF_Tactics <> rank def
R4173:4176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4187:4187 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4167:4170 LamSF_Tactics <> rank def
R4183:4185 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4177:4180 LamSF_Tactics <> rank def
R3973:3997 Extensional_to_combinator <> to_combinator_rank_stable thm
R4216:4219 SF_reduction <> star def
R4200:4203 LamSF_Tactics <> rank def
R4206:4209 SF_reduction <> star def
R4000:4003 Coq.Init.Peano <> pred syndef
R4023:4038 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4195:4195 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4017:4020 LamSF_Tactics <> rank def
R4045:4061 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4194:4194 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4039:4042 LamSF_Tactics <> rank def
R4068:4085 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4193:4193 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4062:4065 LamSF_Tactics <> rank def
R4092:4110 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4192:4192 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4086:4089 LamSF_Tactics <> rank def
R4117:4136 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4191:4191 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4111:4114 LamSF_Tactics <> rank def
R4143:4146 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4190:4190 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4137:4140 LamSF_Tactics <> rank def
R4153:4156 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4189:4189 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4147:4150 LamSF_Tactics <> rank def
R4163:4166 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4188:4188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4157:4160 LamSF_Tactics <> rank def
R4173:4176 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4187:4187 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4167:4170 LamSF_Tactics <> rank def
R4183:4185 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4177:4180 LamSF_Tactics <> rank def
R4253:4255 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4241:4244 LamSF_Tactics <> rank def
R4246:4249 SF_reduction <> star def
R4256:4259 LamSF_Tactics <> rank def
R4262:4264 LamSF_Terms <> Abs constr
R4253:4255 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4241:4244 LamSF_Tactics <> rank def
R4246:4249 SF_reduction <> star def
R4256:4259 LamSF_Tactics <> rank def
R4262:4264 LamSF_Terms <> Abs constr
R4281:4289 SF_reduction <> rank_star thm
prf 4331:4347 <> to_combinator_app
R4386:4388 Coq.Init.Logic <> :type_scope:x_'='_x not
R4363:4375 Extensional_to_combinator <> to_combinator def
R4378:4380 LamSF_Terms <> App constr
R4384:4384 Extensional_to_combinator <> N var
R4382:4382 Extensional_to_combinator <> M var
R4389:4391 LamSF_Terms <> App constr
R4412:4424 Extensional_to_combinator <> to_combinator def
R4426:4426 Extensional_to_combinator <> N var
R4394:4406 Extensional_to_combinator <> to_combinator def
R4408:4408 Extensional_to_combinator <> M var
R4457:4469 Extensional_to_combinator <> to_combinator def
R4472:4475 LamSF_Tactics <> rank def
R4478:4495 Extensional_to_combinator <> to_combinator_rank def
R4503:4520 Extensional_to_combinator <> to_combinator_rank def
R4528:4531 LamSF_Tactics <> rank def
R4503:4520 Extensional_to_combinator <> to_combinator_rank def
R4528:4531 LamSF_Tactics <> rank def
R4548:4549 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4542:4545 LamSF_Tactics <> rank def
R4548:4549 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4542:4545 LamSF_Tactics <> rank def
R4564:4576 LamSF_Tactics <> rank_positive thm
R4602:4604 Coq.Init.Logic <> :type_scope:x_'='_x not
R4593:4595 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4587:4590 LamSF_Tactics <> rank def
R4596:4599 LamSF_Tactics <> rank def
R4605:4605 Coq.Init.Datatypes <> S constr
R4608:4611 Coq.Init.Peano <> pred syndef
R4620:4622 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4614:4617 LamSF_Tactics <> rank def
R4623:4626 LamSF_Tactics <> rank def
R4602:4604 Coq.Init.Logic <> :type_scope:x_'='_x not
R4593:4595 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4587:4590 LamSF_Tactics <> rank def
R4596:4599 LamSF_Tactics <> rank def
R4605:4605 Coq.Init.Datatypes <> S constr
R4608:4611 Coq.Init.Peano <> pred syndef
R4620:4622 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4614:4617 LamSF_Tactics <> rank def
R4623:4626 LamSF_Tactics <> rank def
R4664:4688 Extensional_to_combinator <> to_combinator_rank_stable thm
R4720:4723 LamSF_Tactics <> rank def
R4691:4691 Coq.Init.Datatypes <> S constr
R4694:4697 Coq.Init.Peano <> pred syndef
R4706:4708 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4700:4703 LamSF_Tactics <> rank def
R4709:4712 LamSF_Tactics <> rank def
R4664:4688 Extensional_to_combinator <> to_combinator_rank_stable thm
R4720:4723 LamSF_Tactics <> rank def
R4691:4691 Coq.Init.Datatypes <> S constr
R4694:4697 Coq.Init.Peano <> pred syndef
R4706:4708 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4700:4703 LamSF_Tactics <> rank def
R4709:4712 LamSF_Tactics <> rank def
R4664:4688 Extensional_to_combinator <> to_combinator_rank_stable thm
R4720:4723 LamSF_Tactics <> rank def
R4691:4691 Coq.Init.Datatypes <> S constr
R4694:4697 Coq.Init.Peano <> pred syndef
R4706:4708 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4700:4703 LamSF_Tactics <> rank def
R4709:4712 LamSF_Tactics <> rank def
R4664:4688 Extensional_to_combinator <> to_combinator_rank_stable thm
R4720:4723 LamSF_Tactics <> rank def
R4691:4691 Coq.Init.Datatypes <> S constr
R4694:4697 Coq.Init.Peano <> pred syndef
R4706:4708 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4700:4703 LamSF_Tactics <> rank def
R4709:4712 LamSF_Tactics <> rank def
R4664:4688 Extensional_to_combinator <> to_combinator_rank_stable thm
R4720:4723 LamSF_Tactics <> rank def
R4691:4691 Coq.Init.Datatypes <> S constr
R4694:4697 Coq.Init.Peano <> pred syndef
R4706:4708 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4700:4703 LamSF_Tactics <> rank def
R4709:4712 LamSF_Tactics <> rank def
R4751:4775 Extensional_to_combinator <> to_combinator_rank_stable thm
R4807:4810 LamSF_Tactics <> rank def
R4778:4778 Coq.Init.Datatypes <> S constr
R4781:4784 Coq.Init.Peano <> pred syndef
R4793:4795 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4787:4790 LamSF_Tactics <> rank def
R4796:4799 LamSF_Tactics <> rank def
R4751:4775 Extensional_to_combinator <> to_combinator_rank_stable thm
R4807:4810 LamSF_Tactics <> rank def
R4778:4778 Coq.Init.Datatypes <> S constr
R4781:4784 Coq.Init.Peano <> pred syndef
R4793:4795 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4787:4790 LamSF_Tactics <> rank def
R4796:4799 LamSF_Tactics <> rank def
R4751:4775 Extensional_to_combinator <> to_combinator_rank_stable thm
R4807:4810 LamSF_Tactics <> rank def
R4778:4778 Coq.Init.Datatypes <> S constr
R4781:4784 Coq.Init.Peano <> pred syndef
R4793:4795 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4787:4790 LamSF_Tactics <> rank def
R4796:4799 LamSF_Tactics <> rank def
R4751:4775 Extensional_to_combinator <> to_combinator_rank_stable thm
R4807:4810 LamSF_Tactics <> rank def
R4778:4778 Coq.Init.Datatypes <> S constr
R4781:4784 Coq.Init.Peano <> pred syndef
R4793:4795 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4787:4790 LamSF_Tactics <> rank def
R4796:4799 LamSF_Tactics <> rank def
R4751:4775 Extensional_to_combinator <> to_combinator_rank_stable thm
R4807:4810 LamSF_Tactics <> rank def
R4778:4778 Coq.Init.Datatypes <> S constr
R4781:4784 Coq.Init.Peano <> pred syndef
R4793:4795 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4787:4790 LamSF_Tactics <> rank def
R4796:4799 LamSF_Tactics <> rank def
prf 4853:4883 <> to_combinator_makes_combinators
R4906:4909 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4910:4919 Combinators <> combinator ind
R4922:4934 Extensional_to_combinator <> to_combinator def
R4936:4936 Extensional_to_combinator <> M var
R4898:4903 LamSF_Closed <> closed def
R4905:4905 Extensional_to_combinator <> M var
R4976:4980 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4989:4992 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4993:5002 Combinators <> combinator ind
R5005:5017 Extensional_to_combinator <> to_combinator def
R5019:5019 Extensional_to_combinator <> M var
R4981:4986 LamSF_Closed <> closed def
R4988:4988 Extensional_to_combinator <> M var
R4966:4969 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4965:4965 Extensional_to_combinator <> p var
R4970:4973 LamSF_Tactics <> rank def
R4975:4975 Extensional_to_combinator <> M var
R4976:4980 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4989:4992 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4993:5002 Combinators <> combinator ind
R5005:5017 Extensional_to_combinator <> to_combinator def
R5019:5019 Extensional_to_combinator <> M var
R4981:4986 LamSF_Closed <> closed def
R4988:4988 Extensional_to_combinator <> M var
R4966:4969 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4965:4965 Extensional_to_combinator <> p var
R4970:4973 LamSF_Tactics <> rank def
R4975:4975 Extensional_to_combinator <> M var
R5032:5037 LamSF_Closed <> closed def
R5099:5100 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5093:5096 LamSF_Tactics <> rank def
R5099:5100 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5093:5096 LamSF_Tactics <> rank def
R5115:5127 LamSF_Tactics <> rank_positive thm
R5145:5150 LamSF_Closed <> closed def
R5229:5241 Extensional_to_combinator <> to_combinator def
R5244:5247 LamSF_Tactics <> rank def
R5250:5267 Extensional_to_combinator <> to_combinator_rank def
R5275:5292 Extensional_to_combinator <> to_combinator_rank def
R5275:5292 Extensional_to_combinator <> to_combinator_rank def
R5324:5340 Extensional_to_combinator <> to_combinator_abs thm
R5324:5340 Extensional_to_combinator <> to_combinator_abs thm
R5324:5340 Extensional_to_combinator <> to_combinator_abs thm
R5377:5379 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5365:5368 LamSF_Tactics <> rank def
R5370:5373 SF_reduction <> star def
R5380:5383 LamSF_Tactics <> rank def
R5386:5388 LamSF_Terms <> Abs constr
R5377:5379 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R5365:5368 LamSF_Tactics <> rank def
R5370:5373 SF_reduction <> star def
R5380:5383 LamSF_Tactics <> rank def
R5386:5388 LamSF_Terms <> Abs constr
R5405:5413 SF_reduction <> rank_star thm
R5432:5442 LamSF_Closed <> maxvar_star thm
R5432:5442 LamSF_Closed <> maxvar_star thm
R5432:5442 LamSF_Closed <> maxvar_star thm
R5483:5495 Extensional_to_combinator <> to_combinator def
R5498:5501 LamSF_Tactics <> rank def
R5504:5521 Extensional_to_combinator <> to_combinator_rank def
R5529:5546 Extensional_to_combinator <> to_combinator_rank def
R5554:5557 LamSF_Tactics <> rank def
R5529:5546 Extensional_to_combinator <> to_combinator_rank def
R5554:5557 LamSF_Tactics <> rank def
R5591:5598 Combinators <> comb_app constr
R5611:5635 Extensional_to_combinator <> to_combinator_rank_stable thm
R5658:5661 LamSF_Tactics <> rank def
R5645:5647 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5638:5641 LamSF_Tactics <> rank def
R5648:5651 LamSF_Tactics <> rank def
R5611:5635 Extensional_to_combinator <> to_combinator_rank_stable thm
R5658:5661 LamSF_Tactics <> rank def
R5645:5647 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5638:5641 LamSF_Tactics <> rank def
R5648:5651 LamSF_Tactics <> rank def
R5611:5635 Extensional_to_combinator <> to_combinator_rank_stable thm
R5658:5661 LamSF_Tactics <> rank def
R5645:5647 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5638:5641 LamSF_Tactics <> rank def
R5648:5651 LamSF_Tactics <> rank def
R5611:5635 Extensional_to_combinator <> to_combinator_rank_stable thm
R5658:5661 LamSF_Tactics <> rank def
R5645:5647 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5638:5641 LamSF_Tactics <> rank def
R5648:5651 LamSF_Tactics <> rank def
R5611:5635 Extensional_to_combinator <> to_combinator_rank_stable thm
R5658:5661 LamSF_Tactics <> rank def
R5645:5647 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5638:5641 LamSF_Tactics <> rank def
R5648:5651 LamSF_Tactics <> rank def
R5716:5740 Extensional_to_combinator <> to_combinator_rank_stable thm
R5763:5766 LamSF_Tactics <> rank def
R5750:5752 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5743:5746 LamSF_Tactics <> rank def
R5753:5756 LamSF_Tactics <> rank def
R5716:5740 Extensional_to_combinator <> to_combinator_rank_stable thm
R5763:5766 LamSF_Tactics <> rank def
R5750:5752 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5743:5746 LamSF_Tactics <> rank def
R5753:5756 LamSF_Tactics <> rank def
R5716:5740 Extensional_to_combinator <> to_combinator_rank_stable thm
R5763:5766 LamSF_Tactics <> rank def
R5750:5752 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5743:5746 LamSF_Tactics <> rank def
R5753:5756 LamSF_Tactics <> rank def
R5716:5740 Extensional_to_combinator <> to_combinator_rank_stable thm
R5763:5766 LamSF_Tactics <> rank def
R5750:5752 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5743:5746 LamSF_Tactics <> rank def
R5753:5756 LamSF_Tactics <> rank def
R5716:5740 Extensional_to_combinator <> to_combinator_rank_stable thm
R5763:5766 LamSF_Tactics <> rank def
R5750:5752 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5743:5746 LamSF_Tactics <> rank def
R5753:5756 LamSF_Tactics <> rank def
prf 5827:5854 <> to_combinator_is_extensional
R5869:5879 Eta <> beta_eta_eq ind
R5884:5896 Extensional_to_combinator <> to_combinator def
R5898:5898 Extensional_to_combinator <> M var
R5881:5881 Extensional_to_combinator <> M var
R5938:5942 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5943:5953 Eta <> beta_eta_eq ind
R5958:5970 Extensional_to_combinator <> to_combinator def
R5972:5972 Extensional_to_combinator <> M var
R5955:5955 Extensional_to_combinator <> M var
R5928:5931 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5927:5927 Extensional_to_combinator <> p var
R5932:5935 LamSF_Tactics <> rank def
R5937:5937 Extensional_to_combinator <> M var
R5938:5942 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5943:5953 Eta <> beta_eta_eq ind
R5958:5970 Extensional_to_combinator <> to_combinator def
R5972:5972 Extensional_to_combinator <> M var
R5955:5955 Extensional_to_combinator <> M var
R5928:5931 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R5927:5927 Extensional_to_combinator <> p var
R5932:5935 LamSF_Tactics <> rank def
R5937:5937 Extensional_to_combinator <> M var
R6038:6039 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6032:6035 LamSF_Tactics <> rank def
R6038:6039 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6032:6035 LamSF_Tactics <> rank def
R6054:6066 LamSF_Tactics <> rank_positive thm
R6117:6127 Eta <> beta_eta_eq ind
R6139:6141 LamSF_Terms <> Abs constr
R6130:6133 SF_reduction <> star def
R6117:6127 Eta <> beta_eta_eq ind
R6139:6141 LamSF_Terms <> Abs constr
R6130:6133 SF_reduction <> star def
R6157:6170 Eta <> star_equiv_abs thm
R6182:6192 Eta <> beta_eta_eq ind
R6203:6206 SF_reduction <> star def
R6195:6197 LamSF_Terms <> Abs constr
R6182:6192 Eta <> beta_eta_eq ind
R6203:6206 SF_reduction <> star def
R6195:6197 LamSF_Terms <> Abs constr
R6222:6232 Eta <> symm_etared constr
R6243:6253 Eta <> beta_eta_eq ind
R6265:6277 Extensional_to_combinator <> to_combinator def
R6280:6283 SF_reduction <> star def
R6256:6259 SF_reduction <> star def
R6243:6253 Eta <> beta_eta_eq ind
R6265:6277 Extensional_to_combinator <> to_combinator def
R6280:6283 SF_reduction <> star def
R6256:6259 SF_reduction <> star def
R6325:6327 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6313:6316 LamSF_Tactics <> rank def
R6318:6321 SF_reduction <> star def
R6328:6331 LamSF_Tactics <> rank def
R6334:6336 LamSF_Terms <> Abs constr
R6325:6327 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6313:6316 LamSF_Tactics <> rank def
R6318:6321 SF_reduction <> star def
R6328:6331 LamSF_Tactics <> rank def
R6334:6336 LamSF_Terms <> Abs constr
R6353:6361 SF_reduction <> rank_star thm
R6378:6380 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6372:6375 LamSF_Tactics <> rank def
R6378:6380 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6372:6375 LamSF_Tactics <> rank def
R6395:6407 LamSF_Tactics <> rank_positive thm
R6439:6449 Eta <> beta_eta_eq ind
R6477:6489 Extensional_to_combinator <> to_combinator def
R6492:6494 LamSF_Terms <> Abs constr
R6452:6464 Extensional_to_combinator <> to_combinator def
R6467:6470 SF_reduction <> star def
R6439:6449 Eta <> beta_eta_eq ind
R6477:6489 Extensional_to_combinator <> to_combinator def
R6492:6494 LamSF_Terms <> Abs constr
R6452:6464 Extensional_to_combinator <> to_combinator def
R6467:6470 SF_reduction <> star def
R6510:6522 Extensional_to_combinator <> to_combinator def
R6525:6542 Extensional_to_combinator <> to_combinator_rank def
R6550:6567 Extensional_to_combinator <> to_combinator_rank def
R6550:6567 Extensional_to_combinator <> to_combinator_rank def
R6590:6592 Coq.Init.Logic <> :type_scope:x_'='_x not
R6578:6581 LamSF_Tactics <> rank def
R6584:6586 LamSF_Terms <> Abs constr
R6593:6593 Coq.Init.Datatypes <> S constr
R6596:6599 Coq.Init.Peano <> pred syndef
R6602:6605 LamSF_Tactics <> rank def
R6608:6610 LamSF_Terms <> Abs constr
R6590:6592 Coq.Init.Logic <> :type_scope:x_'='_x not
R6578:6581 LamSF_Tactics <> rank def
R6584:6586 LamSF_Terms <> Abs constr
R6593:6593 Coq.Init.Datatypes <> S constr
R6596:6599 Coq.Init.Peano <> pred syndef
R6602:6605 LamSF_Tactics <> rank def
R6608:6610 LamSF_Terms <> Abs constr
R6645:6647 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6639:6642 LamSF_Tactics <> rank def
R6645:6647 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6639:6642 LamSF_Tactics <> rank def
R6662:6674 LamSF_Tactics <> rank_positive thm
R6716:6740 Extensional_to_combinator <> to_combinator_rank_stable thm
R6943:6946 LamSF_Tactics <> rank def
R6949:6952 SF_reduction <> star def
R6743:6746 Coq.Init.Peano <> pred syndef
R6766:6781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6938:6938 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6760:6763 LamSF_Tactics <> rank def
R6788:6804 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6937:6937 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6782:6785 LamSF_Tactics <> rank def
R6811:6828 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6936:6936 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6805:6808 LamSF_Tactics <> rank def
R6835:6853 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6935:6935 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6829:6832 LamSF_Tactics <> rank def
R6860:6879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6934:6934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6854:6857 LamSF_Tactics <> rank def
R6886:6889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6933:6933 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6880:6883 LamSF_Tactics <> rank def
R6896:6899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6932:6932 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6890:6893 LamSF_Tactics <> rank def
R6906:6909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6931:6931 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6900:6903 LamSF_Tactics <> rank def
R6916:6919 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6930:6930 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6910:6913 LamSF_Tactics <> rank def
R6926:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6920:6923 LamSF_Tactics <> rank def
R6716:6740 Extensional_to_combinator <> to_combinator_rank_stable thm
R6943:6946 LamSF_Tactics <> rank def
R6949:6952 SF_reduction <> star def
R6743:6746 Coq.Init.Peano <> pred syndef
R6766:6781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6938:6938 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6760:6763 LamSF_Tactics <> rank def
R6788:6804 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6937:6937 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6782:6785 LamSF_Tactics <> rank def
R6811:6828 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6936:6936 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6805:6808 LamSF_Tactics <> rank def
R6835:6853 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6935:6935 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6829:6832 LamSF_Tactics <> rank def
R6860:6879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6934:6934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6854:6857 LamSF_Tactics <> rank def
R6886:6889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6933:6933 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6880:6883 LamSF_Tactics <> rank def
R6896:6899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6932:6932 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6890:6893 LamSF_Tactics <> rank def
R6906:6909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6931:6931 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6900:6903 LamSF_Tactics <> rank def
R6916:6919 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6930:6930 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6910:6913 LamSF_Tactics <> rank def
R6926:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6920:6923 LamSF_Tactics <> rank def
R6716:6740 Extensional_to_combinator <> to_combinator_rank_stable thm
R6943:6946 LamSF_Tactics <> rank def
R6949:6952 SF_reduction <> star def
R6743:6746 Coq.Init.Peano <> pred syndef
R6766:6781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6938:6938 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6760:6763 LamSF_Tactics <> rank def
R6788:6804 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6937:6937 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6782:6785 LamSF_Tactics <> rank def
R6811:6828 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6936:6936 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6805:6808 LamSF_Tactics <> rank def
R6835:6853 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6935:6935 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6829:6832 LamSF_Tactics <> rank def
R6860:6879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6934:6934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6854:6857 LamSF_Tactics <> rank def
R6886:6889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6933:6933 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6880:6883 LamSF_Tactics <> rank def
R6896:6899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6932:6932 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6890:6893 LamSF_Tactics <> rank def
R6906:6909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6931:6931 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6900:6903 LamSF_Tactics <> rank def
R6916:6919 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6930:6930 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6910:6913 LamSF_Tactics <> rank def
R6926:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6920:6923 LamSF_Tactics <> rank def
R6716:6740 Extensional_to_combinator <> to_combinator_rank_stable thm
R6943:6946 LamSF_Tactics <> rank def
R6949:6952 SF_reduction <> star def
R6743:6746 Coq.Init.Peano <> pred syndef
R6766:6781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6938:6938 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6760:6763 LamSF_Tactics <> rank def
R6788:6804 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6937:6937 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6782:6785 LamSF_Tactics <> rank def
R6811:6828 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6936:6936 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6805:6808 LamSF_Tactics <> rank def
R6835:6853 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6935:6935 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6829:6832 LamSF_Tactics <> rank def
R6860:6879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6934:6934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6854:6857 LamSF_Tactics <> rank def
R6886:6889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6933:6933 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6880:6883 LamSF_Tactics <> rank def
R6896:6899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6932:6932 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6890:6893 LamSF_Tactics <> rank def
R6906:6909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6931:6931 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6900:6903 LamSF_Tactics <> rank def
R6916:6919 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6930:6930 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6910:6913 LamSF_Tactics <> rank def
R6926:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6920:6923 LamSF_Tactics <> rank def
R6716:6740 Extensional_to_combinator <> to_combinator_rank_stable thm
R6943:6946 LamSF_Tactics <> rank def
R6949:6952 SF_reduction <> star def
R6743:6746 Coq.Init.Peano <> pred syndef
R6766:6781 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6938:6938 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6760:6763 LamSF_Tactics <> rank def
R6788:6804 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6937:6937 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6782:6785 LamSF_Tactics <> rank def
R6811:6828 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6936:6936 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6805:6808 LamSF_Tactics <> rank def
R6835:6853 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6935:6935 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6829:6832 LamSF_Tactics <> rank def
R6860:6879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6934:6934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6854:6857 LamSF_Tactics <> rank def
R6886:6889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6933:6933 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6880:6883 LamSF_Tactics <> rank def
R6896:6899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6932:6932 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6890:6893 LamSF_Tactics <> rank def
R6906:6909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6931:6931 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6900:6903 LamSF_Tactics <> rank def
R6916:6919 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6930:6930 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6910:6913 LamSF_Tactics <> rank def
R6926:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6920:6923 LamSF_Tactics <> rank def
R6988:6990 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6975:6978 LamSF_Tactics <> rank def
R6981:6984 SF_reduction <> star def
R6991:6994 LamSF_Tactics <> rank def
R6997:6999 LamSF_Terms <> Abs constr
R6988:6990 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6975:6978 LamSF_Tactics <> rank def
R6981:6984 SF_reduction <> star def
R6991:6994 LamSF_Tactics <> rank def
R6997:6999 LamSF_Terms <> Abs constr
R7016:7024 SF_reduction <> rank_star thm
R7077:7089 Extensional_to_combinator <> to_combinator def
R7092:7109 Extensional_to_combinator <> to_combinator_rank def
R7117:7134 Extensional_to_combinator <> to_combinator_rank def
R7117:7134 Extensional_to_combinator <> to_combinator_rank def
R7159:7161 Coq.Init.Logic <> :type_scope:x_'='_x not
R7144:7147 LamSF_Tactics <> rank def
R7149:7151 LamSF_Terms <> App constr
R7162:7162 Coq.Init.Datatypes <> S constr
R7165:7168 Coq.Init.Peano <> pred syndef
R7171:7174 LamSF_Tactics <> rank def
R7177:7179 LamSF_Terms <> App constr
R7159:7161 Coq.Init.Logic <> :type_scope:x_'='_x not
R7144:7147 LamSF_Tactics <> rank def
R7149:7151 LamSF_Terms <> App constr
R7162:7162 Coq.Init.Datatypes <> S constr
R7165:7168 Coq.Init.Peano <> pred syndef
R7171:7174 LamSF_Tactics <> rank def
R7177:7179 LamSF_Terms <> App constr
R7216:7218 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7200:7203 LamSF_Tactics <> rank def
R7206:7208 LamSF_Terms <> App constr
R7216:7218 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7200:7203 LamSF_Tactics <> rank def
R7206:7208 LamSF_Terms <> App constr
R7233:7245 LamSF_Tactics <> rank_positive thm
R7290:7299 Eta <> app_etared constr
R7312:7336 Extensional_to_combinator <> to_combinator_rank_stable thm
R7359:7362 LamSF_Tactics <> rank def
R7346:7348 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7339:7342 LamSF_Tactics <> rank def
R7349:7352 LamSF_Tactics <> rank def
R7312:7336 Extensional_to_combinator <> to_combinator_rank_stable thm
R7359:7362 LamSF_Tactics <> rank def
R7346:7348 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7339:7342 LamSF_Tactics <> rank def
R7349:7352 LamSF_Tactics <> rank def
R7312:7336 Extensional_to_combinator <> to_combinator_rank_stable thm
R7359:7362 LamSF_Tactics <> rank def
R7346:7348 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7339:7342 LamSF_Tactics <> rank def
R7349:7352 LamSF_Tactics <> rank def
R7312:7336 Extensional_to_combinator <> to_combinator_rank_stable thm
R7359:7362 LamSF_Tactics <> rank def
R7346:7348 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7339:7342 LamSF_Tactics <> rank def
R7349:7352 LamSF_Tactics <> rank def
R7312:7336 Extensional_to_combinator <> to_combinator_rank_stable thm
R7359:7362 LamSF_Tactics <> rank def
R7346:7348 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7339:7342 LamSF_Tactics <> rank def
R7349:7352 LamSF_Tactics <> rank def
R7417:7441 Extensional_to_combinator <> to_combinator_rank_stable thm
R7464:7467 LamSF_Tactics <> rank def
R7451:7453 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7444:7447 LamSF_Tactics <> rank def
R7454:7457 LamSF_Tactics <> rank def
R7417:7441 Extensional_to_combinator <> to_combinator_rank_stable thm
R7464:7467 LamSF_Tactics <> rank def
R7451:7453 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7444:7447 LamSF_Tactics <> rank def
R7454:7457 LamSF_Tactics <> rank def
R7417:7441 Extensional_to_combinator <> to_combinator_rank_stable thm
R7464:7467 LamSF_Tactics <> rank def
R7451:7453 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7444:7447 LamSF_Tactics <> rank def
R7454:7457 LamSF_Tactics <> rank def
R7417:7441 Extensional_to_combinator <> to_combinator_rank_stable thm
R7464:7467 LamSF_Tactics <> rank def
R7451:7453 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7444:7447 LamSF_Tactics <> rank def
R7454:7457 LamSF_Tactics <> rank def
R7417:7441 Extensional_to_combinator <> to_combinator_rank_stable thm
R7464:7467 LamSF_Tactics <> rank def
R7451:7453 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7444:7447 LamSF_Tactics <> rank def
R7454:7457 LamSF_Tactics <> rank def
def 7531:7540 <> to_comb_fn
R7546:7548 LamSF_Terms <> Abs constr
R7551:7553 LamSF_Terms <> Abs constr
R7557:7559 LamSF_Terms <> App constr
R7599:7601 LamSF_Terms <> Abs constr
R7604:7606 LamSF_Terms <> Abs constr
R7610:7612 LamSF_Terms <> App constr
R7678:7680 LamSF_Terms <> App constr
R7705:7707 LamSF_Terms <> App constr
R7718:7720 LamSF_Terms <> Ref constr
R7710:7712 LamSF_Terms <> Ref constr
R7683:7685 LamSF_Terms <> App constr
R7696:7698 LamSF_Terms <> Ref constr
R7688:7690 LamSF_Terms <> Ref constr
R7615:7617 LamSF_Terms <> App constr
R7655:7657 LamSF_Terms <> App constr
R7668:7670 LamSF_Terms <> Ref constr
R7660:7662 LamSF_Terms <> Ref constr
R7620:7622 LamSF_Terms <> App constr
R7646:7648 LamSF_Terms <> Ref constr
R7625:7627 LamSF_Terms <> App constr
R7635:7642 SF_reduction <> abs_left def
R7629:7633 Equal <> equal def
R7562:7564 LamSF_Terms <> App constr
R7590:7592 LamSF_Terms <> Ref constr
R7567:7569 LamSF_Terms <> App constr
R7581:7583 LamSF_Terms <> Ref constr
R7572:7573 LamSF_Terms <> Op constr
R7575:7577 LamSF_Terms <> Fop constr
def 7746:7752 <> to_comb
R7757:7759 LamSF_Terms <> App constr
R7770:7779 Extensional_to_combinator <> to_comb_fn def
R7761:7768 LamSF_Eval <> fixpoint def
prf 7790:7799 <> to_comb_op
R7813:7821 LamSF_reduction <> lamSF_red def
R7845:7846 LamSF_Terms <> Op constr
R7848:7848 Extensional_to_combinator <> o var
R7824:7826 LamSF_Terms <> App constr
R7837:7838 LamSF_Terms <> Op constr
R7840:7840 Extensional_to_combinator <> o var
R7828:7834 Extensional_to_combinator <> to_comb def
R7879:7885 Extensional_to_combinator <> to_comb def
R7901:7907 Extensional_to_combinator <> to_comb def
R7901:7907 Extensional_to_combinator <> to_comb def
R7918:7927 Extensional_to_combinator <> to_comb_fn def
prf 7981:7991 <> to_comb_abs
R8012:8015 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8034:8038 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8039:8047 LamSF_reduction <> lamSF_red def
R8072:8074 LamSF_Terms <> App constr
R8085:8088 SF_reduction <> star def
R8090:8090 Extensional_to_combinator <> M var
R8076:8082 Extensional_to_combinator <> to_comb def
R8050:8052 LamSF_Terms <> App constr
R8063:8065 LamSF_Terms <> Abs constr
R8067:8067 Extensional_to_combinator <> M var
R8054:8060 Extensional_to_combinator <> to_comb def
R8030:8032 Coq.Init.Logic <> :type_scope:x_'='_x not
R8016:8021 LamSF_Closed <> maxvar def
R8024:8026 LamSF_Terms <> Abs constr
R8028:8028 Extensional_to_combinator <> M var
R8004:8009 LamSF_Normal <> normal ind
R8011:8011 Extensional_to_combinator <> M var
R8122:8128 Extensional_to_combinator <> to_comb def
R8146:8155 Extensional_to_combinator <> to_comb_fn def
R8168:8174 Extensional_to_combinator <> to_comb def
R8168:8174 Extensional_to_combinator <> to_comb def
R8197:8205 LamSF_Terms <> subst_rec def
R8213:8221 LamSF_Terms <> subst_rec def
R8213:8221 LamSF_Terms <> subst_rec def
R8248:8260 LamSF_Substitution_term <> lift_rec_null thm
R8248:8260 LamSF_Substitution_term <> lift_rec_null thm
R8248:8260 LamSF_Substitution_term <> lift_rec_null thm
R8286:8295 LamSF_Tactics <> multi_step ind
R8309:8311 LamSF_Terms <> App constr
R8314:8316 LamSF_Terms <> App constr
R8319:8321 LamSF_Terms <> App constr
R8324:8325 LamSF_Terms <> Op constr
R8327:8329 LamSF_Terms <> Fop constr
R8297:8306 LamSF_reduction <> lamSF_red1 ind
R8286:8295 LamSF_Tactics <> multi_step ind
R8309:8311 LamSF_Terms <> App constr
R8314:8316 LamSF_Terms <> App constr
R8319:8321 LamSF_Terms <> App constr
R8324:8325 LamSF_Terms <> Op constr
R8327:8329 LamSF_Terms <> Fop constr
R8297:8306 LamSF_reduction <> lamSF_red1 ind
R8372:8374 LamSF_Terms <> App constr
R8404:8418 SF_reduction <> right_component def