forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Intensional_to_combinator.glob
3498 lines (3498 loc) · 162 KB
/
Intensional_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 9e95372c4288d1366799b0bc6cfb144f
FIntensional_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:2483 Extensional_to_combinator <> <> lib
R2501:2506 Unstar <> <> lib
R2525:2531 Binding <> <> lib
R2550:2554 Coq.omega.Omega <> <> lib
def 2822:2839 <> is_combinator_bool
R2853:2853 Intensional_to_combinator <> M var
R2863:2864 LamSF_Terms <> Op constr
R2871:2874 Coq.Init.Datatypes <> true constr
R2879:2881 LamSF_Terms <> App constr
R2892:2895 Coq.Init.Datatypes <> andb def
R2922:2939 Intensional_to_combinator <> is_combinator_bool def
R2898:2915 Intensional_to_combinator <> is_combinator_bool def
R2952:2956 Coq.Init.Datatypes <> false constr
prf 2971:2993 <> is_combinator_bool_true
R3018:3021 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3042:3044 Coq.Init.Logic <> :type_scope:x_'='_x not
R3022:3039 Intensional_to_combinator <> is_combinator_bool def
R3041:3041 Intensional_to_combinator <> M var
R3045:3048 Coq.Init.Datatypes <> true constr
R3006:3015 Combinators <> combinator ind
R3017:3017 Intensional_to_combinator <> M var
prf 3139:3162 <> is_combinator_bool_false
R3175:3175 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3197:3201 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3222:3224 Coq.Init.Logic <> :type_scope:x_'='_x not
R3202:3219 Intensional_to_combinator <> is_combinator_bool def
R3221:3221 Intensional_to_combinator <> M var
R3225:3229 Coq.Init.Datatypes <> false constr
R3188:3191 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3192:3196 Coq.Init.Logic <> False ind
R3176:3185 Combinators <> combinator ind
R3187:3187 Intensional_to_combinator <> M var
R3275:3279 Coq.Init.Logic <> False ind
R3275:3279 Coq.Init.Logic <> False ind
R3275:3279 Coq.Init.Logic <> False ind
R3323:3327 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3350:3350 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3310:3319 Combinators <> combinator ind
R3341:3344 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3345:3349 Coq.Init.Logic <> False ind
R3328:3337 Combinators <> combinator ind
R3323:3327 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3350:3350 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3310:3319 Combinators <> combinator ind
R3341:3344 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3345:3349 Coq.Init.Logic <> False ind
R3328:3337 Combinators <> combinator ind
R3364:3383 Combinators <> combinator_decidable thm
R3434:3438 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3461:3461 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3421:3430 Combinators <> combinator ind
R3452:3455 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3456:3460 Coq.Init.Logic <> False ind
R3439:3448 Combinators <> combinator ind
R3434:3438 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3461:3461 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R3421:3430 Combinators <> combinator ind
R3452:3455 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3456:3460 Coq.Init.Logic <> False ind
R3439:3448 Combinators <> combinator ind
R3475:3494 Combinators <> combinator_decidable thm
R3532:3536 Coq.Init.Logic <> False ind
R3532:3536 Coq.Init.Logic <> False ind
R3581:3598 Intensional_to_combinator <> is_combinator_bool def
R3581:3598 Intensional_to_combinator <> is_combinator_bool def
def 3674:3695 <> to_combinator_int_rank
R3711:3711 Intensional_to_combinator <> p var
R3726:3726 Intensional_to_combinator <> M var
R3731:3731 Coq.Init.Datatypes <> S constr
R3745:3745 Intensional_to_combinator <> M var
R3755:3757 LamSF_Terms <> Ref constr
R3764:3766 LamSF_Terms <> Ref constr
R3773:3774 LamSF_Terms <> Op constr
R3781:3782 LamSF_Terms <> Op constr
R3789:3791 LamSF_Terms <> Abs constr
R3806:3811 LamSF_Closed <> maxvar def
R3829:3835 Unstar <> abs_tag def
R3838:3859 Intensional_to_combinator <> to_combinator_int_rank def
R3864:3866 LamSF_Terms <> App constr
R3868:3871 SF_reduction <> k_op def
R3885:3891 Unstar <> abs_tag def
R3894:3915 Intensional_to_combinator <> to_combinator_int_rank def
R3920:3923 SF_reduction <> star def
R3936:3938 LamSF_Terms <> App constr
R3953:3970 Intensional_to_combinator <> is_combinator_bool def
R3973:3975 LamSF_Terms <> App constr
R4047:4053 Unstar <> app_tag def
R4086:4107 Intensional_to_combinator <> to_combinator_int_rank def
R4056:4077 Intensional_to_combinator <> to_combinator_int_rank def
R4006:4012 Unstar <> com_tag def
R4015:4017 LamSF_Terms <> App constr
def 4137:4153 <> to_combinator_int
R4160:4181 Intensional_to_combinator <> to_combinator_int_rank def
R4192:4192 Intensional_to_combinator <> M var
R4184:4187 LamSF_Tactics <> rank def
R4189:4189 Intensional_to_combinator <> M var
prf 4205:4233 <> to_combinator_int_rank_stable
R4256:4259 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4271:4274 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4301:4303 Coq.Init.Logic <> :type_scope:x_'='_x not
R4275:4296 Intensional_to_combinator <> to_combinator_int_rank def
R4300:4300 Intensional_to_combinator <> M var
R4298:4298 Intensional_to_combinator <> p var
R4304:4325 Intensional_to_combinator <> to_combinator_int_rank def
R4329:4329 Intensional_to_combinator <> M var
R4327:4327 Intensional_to_combinator <> q var
R4261:4264 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4260:4260 Intensional_to_combinator <> q var
R4265:4268 LamSF_Tactics <> rank def
R4270:4270 Intensional_to_combinator <> M var
R4252:4254 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4251:4251 Intensional_to_combinator <> p var
R4255:4255 Intensional_to_combinator <> q var
R4379:4380 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4373:4376 LamSF_Tactics <> rank def
R4379:4380 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4373:4376 LamSF_Tactics <> rank def
R4395:4407 LamSF_Tactics <> rank_positive thm
R4451:4453 Coq.Init.Logic <> :type_scope:x_'='_x not
R4454:4454 Coq.Init.Datatypes <> S constr
R4456:4459 Coq.Init.Peano <> pred syndef
R4451:4453 Coq.Init.Logic <> :type_scope:x_'='_x not
R4454:4454 Coq.Init.Datatypes <> S constr
R4456:4459 Coq.Init.Peano <> pred syndef
R4512:4514 Coq.Init.Logic <> :type_scope:x_'='_x not
R4515:4515 Coq.Init.Datatypes <> S constr
R4517:4520 Coq.Init.Peano <> pred syndef
R4512:4514 Coq.Init.Logic <> :type_scope:x_'='_x not
R4515:4515 Coq.Init.Datatypes <> S constr
R4517:4520 Coq.Init.Peano <> pred syndef
R4578:4580 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4572:4575 LamSF_Tactics <> rank def
R4578:4580 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4572:4575 LamSF_Tactics <> rank def
R4595:4607 LamSF_Tactics <> rank_positive thm
R4619:4621 Coq.Init.Logic <> :type_scope:x_'='_x not
R4622:4622 Coq.Init.Datatypes <> S constr
R4624:4627 Coq.Init.Peano <> pred syndef
R4619:4621 Coq.Init.Logic <> :type_scope:x_'='_x not
R4622:4622 Coq.Init.Datatypes <> S constr
R4624:4627 Coq.Init.Peano <> pred syndef
R4670:4675 LamSF_Closed <> maxvar def
R4670:4675 LamSF_Closed <> maxvar def
R4707:4710 Coq.Init.Peano <> pred syndef
R4707:4710 Coq.Init.Peano <> pred syndef
R4707:4710 Coq.Init.Peano <> pred syndef
R4707:4710 Coq.Init.Peano <> pred syndef
R4707:4710 Coq.Init.Peano <> pred syndef
R4759:4762 Coq.Init.Peano <> pred syndef
R4759:4762 Coq.Init.Peano <> pred syndef
R4759:4762 Coq.Init.Peano <> pred syndef
R4759:4762 Coq.Init.Peano <> pred syndef
R4759:4762 Coq.Init.Peano <> pred syndef
R4802:4804 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4790:4793 LamSF_Tactics <> rank def
R4795:4798 SF_reduction <> star def
R4805:4808 LamSF_Tactics <> rank def
R4811:4813 LamSF_Terms <> Abs constr
R4802:4804 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R4790:4793 LamSF_Tactics <> rank def
R4795:4798 SF_reduction <> star def
R4805:4808 LamSF_Tactics <> rank def
R4811:4813 LamSF_Terms <> Abs constr
R4830:4838 SF_reduction <> rank_star thm
R4880:4882 Coq.Init.Logic <> :type_scope:x_'='_x not
R4883:4883 Coq.Init.Datatypes <> S constr
R4885:4888 Coq.Init.Peano <> pred syndef
R4880:4882 Coq.Init.Logic <> :type_scope:x_'='_x not
R4883:4883 Coq.Init.Datatypes <> S constr
R4885:4888 Coq.Init.Peano <> pred syndef
R4931:4948 Intensional_to_combinator <> is_combinator_bool def
R4931:4948 Intensional_to_combinator <> is_combinator_bool def
R4972:4989 Intensional_to_combinator <> is_combinator_bool def
R4972:4989 Intensional_to_combinator <> is_combinator_bool def
R5022:5025 Coq.Init.Peano <> pred syndef
R5022:5025 Coq.Init.Peano <> pred syndef
R5022:5025 Coq.Init.Peano <> pred syndef
R5022:5025 Coq.Init.Peano <> pred syndef
R5022:5025 Coq.Init.Peano <> pred syndef
R5060:5063 Coq.Init.Peano <> pred syndef
R5060:5063 Coq.Init.Peano <> pred syndef
R5060:5063 Coq.Init.Peano <> pred syndef
R5060:5063 Coq.Init.Peano <> pred syndef
R5060:5063 Coq.Init.Peano <> pred syndef
R5106:5109 Coq.Init.Peano <> pred syndef
R5106:5109 Coq.Init.Peano <> pred syndef
R5106:5109 Coq.Init.Peano <> pred syndef
R5106:5109 Coq.Init.Peano <> pred syndef
R5106:5109 Coq.Init.Peano <> pred syndef
R5144:5147 Coq.Init.Peano <> pred syndef
R5144:5147 Coq.Init.Peano <> pred syndef
R5144:5147 Coq.Init.Peano <> pred syndef
R5144:5147 Coq.Init.Peano <> pred syndef
R5144:5147 Coq.Init.Peano <> pred syndef
prf 5189:5211 <> to_combinator_int_abs_0
R5232:5235 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5261:5263 Coq.Init.Logic <> :type_scope:x_'='_x not
R5236:5252 Intensional_to_combinator <> to_combinator_int def
R5255:5257 LamSF_Terms <> Abs constr
R5259:5259 Intensional_to_combinator <> M var
R5264:5270 Unstar <> abs_tag def
R5273:5289 Intensional_to_combinator <> to_combinator_int def
R5292:5294 LamSF_Terms <> App constr
R5301:5301 Intensional_to_combinator <> M var
R5296:5299 SF_reduction <> k_op def
R5224:5229 LamSF_Closed <> closed def
R5231:5231 Intensional_to_combinator <> M var
R5331:5347 Intensional_to_combinator <> to_combinator_int def
R5363:5366 LamSF_Tactics <> rank def
R5369:5390 Intensional_to_combinator <> to_combinator_int_rank def
R5398:5419 Intensional_to_combinator <> to_combinator_int_rank def
R5427:5430 LamSF_Tactics <> rank def
R5398:5419 Intensional_to_combinator <> to_combinator_int_rank def
R5427:5430 LamSF_Tactics <> rank def
R5447:5448 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5441:5444 LamSF_Tactics <> rank def
R5447:5448 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5441:5444 LamSF_Tactics <> rank def
R5463:5475 LamSF_Tactics <> rank_positive thm
R5503:5505 Coq.Init.Logic <> :type_scope:x_'='_x not
R5494:5496 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5486:5493 LamSF_Tactics <> abs_rank def
R5497:5500 LamSF_Tactics <> rank def
R5506:5506 Coq.Init.Datatypes <> S constr
R5509:5512 Coq.Init.Peano <> pred syndef
R5523:5525 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5515:5522 LamSF_Tactics <> abs_rank def
R5526:5529 LamSF_Tactics <> rank def
R5503:5505 Coq.Init.Logic <> :type_scope:x_'='_x not
R5494:5496 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5486:5493 LamSF_Tactics <> abs_rank def
R5497:5500 LamSF_Tactics <> rank def
R5506:5506 Coq.Init.Datatypes <> S constr
R5509:5512 Coq.Init.Peano <> pred syndef
R5523:5525 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R5515:5522 LamSF_Tactics <> abs_rank def
R5526:5529 LamSF_Tactics <> rank def
R5546:5553 LamSF_Tactics <> abs_rank def
R5585:5606 Intensional_to_combinator <> to_combinator_int_rank def
R5619:5640 Intensional_to_combinator <> to_combinator_int_rank def
R5619:5640 Intensional_to_combinator <> to_combinator_int_rank def
R5673:5689 Intensional_to_combinator <> to_combinator_int def
R5702:5730 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R5933:5936 LamSF_Tactics <> rank def
R5939:5941 LamSF_Terms <> App constr
R5943:5946 SF_reduction <> k_op def
R5733:5736 Coq.Init.Peano <> pred syndef
R5756:5771 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5928:5928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5750:5753 LamSF_Tactics <> rank def
R5778:5794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5927:5927 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5772:5775 LamSF_Tactics <> rank def
R5801:5818 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5926:5926 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5795:5798 LamSF_Tactics <> rank def
R5825:5843 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5925:5925 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5819:5822 LamSF_Tactics <> rank def
R5850:5869 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5924:5924 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5844:5847 LamSF_Tactics <> rank def
R5876:5879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5923:5923 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5870:5873 LamSF_Tactics <> rank def
R5886:5889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5922:5922 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5880:5883 LamSF_Tactics <> rank def
R5896:5899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5921:5921 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5890:5893 LamSF_Tactics <> rank def
R5906:5909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5920:5920 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5900:5903 LamSF_Tactics <> rank def
R5916:5918 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5910:5913 LamSF_Tactics <> rank def
R5702:5730 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R5933:5936 LamSF_Tactics <> rank def
R5939:5941 LamSF_Terms <> App constr
R5943:5946 SF_reduction <> k_op def
R5733:5736 Coq.Init.Peano <> pred syndef
R5756:5771 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5928:5928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5750:5753 LamSF_Tactics <> rank def
R5778:5794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5927:5927 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5772:5775 LamSF_Tactics <> rank def
R5801:5818 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5926:5926 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5795:5798 LamSF_Tactics <> rank def
R5825:5843 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5925:5925 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5819:5822 LamSF_Tactics <> rank def
R5850:5869 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5924:5924 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5844:5847 LamSF_Tactics <> rank def
R5876:5879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5923:5923 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5870:5873 LamSF_Tactics <> rank def
R5886:5889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5922:5922 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5880:5883 LamSF_Tactics <> rank def
R5896:5899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5921:5921 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5890:5893 LamSF_Tactics <> rank def
R5906:5909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5920:5920 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5900:5903 LamSF_Tactics <> rank def
R5916:5918 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5910:5913 LamSF_Tactics <> rank def
R5702:5730 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R5933:5936 LamSF_Tactics <> rank def
R5939:5941 LamSF_Terms <> App constr
R5943:5946 SF_reduction <> k_op def
R5733:5736 Coq.Init.Peano <> pred syndef
R5756:5771 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5928:5928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5750:5753 LamSF_Tactics <> rank def
R5778:5794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5927:5927 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5772:5775 LamSF_Tactics <> rank def
R5801:5818 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5926:5926 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5795:5798 LamSF_Tactics <> rank def
R5825:5843 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5925:5925 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5819:5822 LamSF_Tactics <> rank def
R5850:5869 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5924:5924 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5844:5847 LamSF_Tactics <> rank def
R5876:5879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5923:5923 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5870:5873 LamSF_Tactics <> rank def
R5886:5889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5922:5922 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5880:5883 LamSF_Tactics <> rank def
R5896:5899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5921:5921 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5890:5893 LamSF_Tactics <> rank def
R5906:5909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5920:5920 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5900:5903 LamSF_Tactics <> rank def
R5916:5918 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5910:5913 LamSF_Tactics <> rank def
R5702:5730 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R5933:5936 LamSF_Tactics <> rank def
R5939:5941 LamSF_Terms <> App constr
R5943:5946 SF_reduction <> k_op def
R5733:5736 Coq.Init.Peano <> pred syndef
R5756:5771 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5928:5928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5750:5753 LamSF_Tactics <> rank def
R5778:5794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5927:5927 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5772:5775 LamSF_Tactics <> rank def
R5801:5818 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5926:5926 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5795:5798 LamSF_Tactics <> rank def
R5825:5843 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5925:5925 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5819:5822 LamSF_Tactics <> rank def
R5850:5869 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5924:5924 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5844:5847 LamSF_Tactics <> rank def
R5876:5879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5923:5923 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5870:5873 LamSF_Tactics <> rank def
R5886:5889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5922:5922 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5880:5883 LamSF_Tactics <> rank def
R5896:5899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5921:5921 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5890:5893 LamSF_Tactics <> rank def
R5906:5909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5920:5920 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5900:5903 LamSF_Tactics <> rank def
R5916:5918 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5910:5913 LamSF_Tactics <> rank def
R5702:5730 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R5933:5936 LamSF_Tactics <> rank def
R5939:5941 LamSF_Terms <> App constr
R5943:5946 SF_reduction <> k_op def
R5733:5736 Coq.Init.Peano <> pred syndef
R5756:5771 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5928:5928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5750:5753 LamSF_Tactics <> rank def
R5778:5794 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5927:5927 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5772:5775 LamSF_Tactics <> rank def
R5801:5818 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5926:5926 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5795:5798 LamSF_Tactics <> rank def
R5825:5843 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5925:5925 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5819:5822 LamSF_Tactics <> rank def
R5850:5869 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5924:5924 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5844:5847 LamSF_Tactics <> rank def
R5876:5879 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5923:5923 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5870:5873 LamSF_Tactics <> rank def
R5886:5889 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5922:5922 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5880:5883 LamSF_Tactics <> rank def
R5896:5899 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5921:5921 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5890:5893 LamSF_Tactics <> rank def
R5906:5909 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5920:5920 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5900:5903 LamSF_Tactics <> rank def
R5916:5918 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5910:5913 LamSF_Tactics <> rank def
prf 5998:6020 <> to_combinator_int_abs_1
R6045:6048 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6074:6076 Coq.Init.Logic <> :type_scope:x_'='_x not
R6049:6065 Intensional_to_combinator <> to_combinator_int def
R6068:6070 LamSF_Terms <> Abs constr
R6072:6072 Intensional_to_combinator <> M var
R6077:6083 Unstar <> abs_tag def
R6086:6102 Intensional_to_combinator <> to_combinator_int def
R6105:6108 SF_reduction <> star def
R6110:6110 Intensional_to_combinator <> M var
R6041:6043 Coq.Init.Logic <> :type_scope:x_'='_x not
R6033:6038 LamSF_Closed <> maxvar def
R6040:6040 Intensional_to_combinator <> M var
R6140:6156 Intensional_to_combinator <> to_combinator_int def
R6172:6175 LamSF_Tactics <> rank def
R6178:6199 Intensional_to_combinator <> to_combinator_int_rank def
R6207:6228 Intensional_to_combinator <> to_combinator_int_rank def
R6236:6239 LamSF_Tactics <> rank def
R6207:6228 Intensional_to_combinator <> to_combinator_int_rank def
R6236:6239 LamSF_Tactics <> rank def
R6256:6257 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6250:6253 LamSF_Tactics <> rank def
R6256:6257 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6250:6253 LamSF_Tactics <> rank def
R6272:6284 LamSF_Tactics <> rank_positive thm
R6312:6314 Coq.Init.Logic <> :type_scope:x_'='_x not
R6303:6305 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6295:6302 LamSF_Tactics <> abs_rank def
R6306:6309 LamSF_Tactics <> rank def
R6315:6315 Coq.Init.Datatypes <> S constr
R6318:6321 Coq.Init.Peano <> pred syndef
R6332:6334 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6324:6331 LamSF_Tactics <> abs_rank def
R6335:6338 LamSF_Tactics <> rank def
R6312:6314 Coq.Init.Logic <> :type_scope:x_'='_x not
R6303:6305 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6295:6302 LamSF_Tactics <> abs_rank def
R6306:6309 LamSF_Tactics <> rank def
R6315:6315 Coq.Init.Datatypes <> S constr
R6318:6321 Coq.Init.Peano <> pred syndef
R6332:6334 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6324:6331 LamSF_Tactics <> abs_rank def
R6335:6338 LamSF_Tactics <> rank def
R6355:6362 LamSF_Tactics <> abs_rank def
R6394:6415 Intensional_to_combinator <> to_combinator_int_rank def
R6428:6449 Intensional_to_combinator <> to_combinator_int_rank def
R6428:6449 Intensional_to_combinator <> to_combinator_int_rank def
R6474:6490 Intensional_to_combinator <> to_combinator_int def
R6503:6531 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R6561:6564 LamSF_Tactics <> rank def
R6567:6570 SF_reduction <> star def
R6534:6537 Coq.Init.Peano <> pred syndef
R6548:6550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6540:6547 LamSF_Tactics <> abs_rank def
R6551:6554 LamSF_Tactics <> rank def
R6503:6531 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R6561:6564 LamSF_Tactics <> rank def
R6567:6570 SF_reduction <> star def
R6534:6537 Coq.Init.Peano <> pred syndef
R6548:6550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6540:6547 LamSF_Tactics <> abs_rank def
R6551:6554 LamSF_Tactics <> rank def
R6503:6531 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R6561:6564 LamSF_Tactics <> rank def
R6567:6570 SF_reduction <> star def
R6534:6537 Coq.Init.Peano <> pred syndef
R6548:6550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6540:6547 LamSF_Tactics <> abs_rank def
R6551:6554 LamSF_Tactics <> rank def
R6503:6531 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R6561:6564 LamSF_Tactics <> rank def
R6567:6570 SF_reduction <> star def
R6534:6537 Coq.Init.Peano <> pred syndef
R6548:6550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6540:6547 LamSF_Tactics <> abs_rank def
R6551:6554 LamSF_Tactics <> rank def
R6503:6531 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R6561:6564 LamSF_Tactics <> rank def
R6567:6570 SF_reduction <> star def
R6534:6537 Coq.Init.Peano <> pred syndef
R6548:6550 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R6540:6547 LamSF_Tactics <> abs_rank def
R6551:6554 LamSF_Tactics <> rank def
R6606:6608 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6593:6596 LamSF_Tactics <> rank def
R6599:6602 SF_reduction <> star def
R6609:6612 LamSF_Tactics <> rank def
R6615:6617 LamSF_Terms <> Abs constr
R6606:6608 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R6593:6596 LamSF_Tactics <> rank def
R6599:6602 SF_reduction <> star def
R6609:6612 LamSF_Tactics <> rank def
R6615:6617 LamSF_Terms <> Abs constr
R6634:6642 SF_reduction <> rank_star thm
R6659:6661 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6653:6656 LamSF_Tactics <> rank def
R6659:6661 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6653:6656 LamSF_Tactics <> rank def
R6676:6688 LamSF_Tactics <> rank_positive thm
R6699:6706 LamSF_Tactics <> abs_rank def
prf 6751:6776 <> to_combinator_int_app_comb
R6812:6815 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6843:6845 Coq.Init.Logic <> :type_scope:x_'='_x not
R6816:6832 Intensional_to_combinator <> to_combinator_int def
R6835:6837 LamSF_Terms <> App constr
R6841:6841 Intensional_to_combinator <> N var
R6839:6839 Intensional_to_combinator <> M var
R6846:6852 Unstar <> com_tag def
R6855:6857 LamSF_Terms <> App constr
R6861:6861 Intensional_to_combinator <> N var
R6859:6859 Intensional_to_combinator <> M var
R6792:6801 Combinators <> combinator ind
R6804:6806 LamSF_Terms <> App constr
R6810:6810 Intensional_to_combinator <> N var
R6808:6808 Intensional_to_combinator <> M var
R6892:6908 Intensional_to_combinator <> to_combinator_int def
R6911:6914 LamSF_Tactics <> rank def
R6917:6938 Intensional_to_combinator <> to_combinator_int_rank def
R6946:6967 Intensional_to_combinator <> to_combinator_int_rank def
R6975:6978 LamSF_Tactics <> rank def
R6946:6967 Intensional_to_combinator <> to_combinator_int_rank def
R6975:6978 LamSF_Tactics <> rank def
R7020:7021 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7014:7017 LamSF_Tactics <> rank def
R7020:7021 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7014:7017 LamSF_Tactics <> rank def
R7036:7048 LamSF_Tactics <> rank_positive thm
R7074:7076 Coq.Init.Logic <> :type_scope:x_'='_x not
R7065:7067 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7059:7062 LamSF_Tactics <> rank def
R7068:7071 LamSF_Tactics <> rank def
R7077:7077 Coq.Init.Datatypes <> S constr
R7080:7083 Coq.Init.Peano <> pred syndef
R7092:7094 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7086:7089 LamSF_Tactics <> rank def
R7095:7098 LamSF_Tactics <> rank def
R7074:7076 Coq.Init.Logic <> :type_scope:x_'='_x not
R7065:7067 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7059:7062 LamSF_Tactics <> rank def
R7068:7071 LamSF_Tactics <> rank def
R7077:7077 Coq.Init.Datatypes <> S constr
R7080:7083 Coq.Init.Peano <> pred syndef
R7092:7094 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7086:7089 LamSF_Tactics <> rank def
R7095:7098 LamSF_Tactics <> rank def
R7124:7146 Intensional_to_combinator <> is_combinator_bool_true thm
R7124:7146 Intensional_to_combinator <> is_combinator_bool_true thm
R7124:7146 Intensional_to_combinator <> is_combinator_bool_true thm
R7124:7146 Intensional_to_combinator <> is_combinator_bool_true thm
R7165:7187 Intensional_to_combinator <> is_combinator_bool_true thm
R7165:7187 Intensional_to_combinator <> is_combinator_bool_true thm
R7165:7187 Intensional_to_combinator <> is_combinator_bool_true thm
R7165:7187 Intensional_to_combinator <> is_combinator_bool_true thm
prf 7223:7252 <> to_combinator_int_app_not_comb
R7268:7268 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7298:7303 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7331:7333 Coq.Init.Logic <> :type_scope:x_'='_x not
R7304:7320 Intensional_to_combinator <> to_combinator_int def
R7323:7325 LamSF_Terms <> App constr
R7329:7329 Intensional_to_combinator <> N var
R7327:7327 Intensional_to_combinator <> M var
R7334:7340 Unstar <> app_tag def
R7365:7381 Intensional_to_combinator <> to_combinator_int def
R7383:7383 Intensional_to_combinator <> N var
R7343:7359 Intensional_to_combinator <> to_combinator_int def
R7361:7361 Intensional_to_combinator <> M var
R7289:7292 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7293:7297 Coq.Init.Logic <> False ind
R7269:7278 Combinators <> combinator ind
R7281:7283 LamSF_Terms <> App constr
R7287:7287 Intensional_to_combinator <> N var
R7285:7285 Intensional_to_combinator <> M var
R7414:7430 Intensional_to_combinator <> to_combinator_int def
R7433:7436 LamSF_Tactics <> rank def
R7439:7460 Intensional_to_combinator <> to_combinator_int_rank def
R7468:7489 Intensional_to_combinator <> to_combinator_int_rank def
R7497:7500 LamSF_Tactics <> rank def
R7468:7489 Intensional_to_combinator <> to_combinator_int_rank def
R7497:7500 LamSF_Tactics <> rank def
R7512:7535 Intensional_to_combinator <> is_combinator_bool_false thm
R7512:7535 Intensional_to_combinator <> is_combinator_bool_false thm
R7512:7535 Intensional_to_combinator <> is_combinator_bool_false thm
R7512:7535 Intensional_to_combinator <> is_combinator_bool_false thm
R7552:7553 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7546:7549 LamSF_Tactics <> rank def
R7552:7553 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7546:7549 LamSF_Tactics <> rank def
R7568:7580 LamSF_Tactics <> rank_positive thm
R7593:7621 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7642:7645 LamSF_Tactics <> rank def
R7630:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7624:7627 LamSF_Tactics <> rank def
R7633:7636 LamSF_Tactics <> rank def
R7593:7621 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7642:7645 LamSF_Tactics <> rank def
R7630:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7624:7627 LamSF_Tactics <> rank def
R7633:7636 LamSF_Tactics <> rank def
R7593:7621 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7642:7645 LamSF_Tactics <> rank def
R7630:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7624:7627 LamSF_Tactics <> rank def
R7633:7636 LamSF_Tactics <> rank def
R7593:7621 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7642:7645 LamSF_Tactics <> rank def
R7630:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7624:7627 LamSF_Tactics <> rank def
R7633:7636 LamSF_Tactics <> rank def
R7593:7621 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7642:7645 LamSF_Tactics <> rank def
R7630:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7624:7627 LamSF_Tactics <> rank def
R7633:7636 LamSF_Tactics <> rank def
R7673:7701 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7721:7724 LamSF_Tactics <> rank def
R7710:7712 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7704:7707 LamSF_Tactics <> rank def
R7713:7716 LamSF_Tactics <> rank def
R7673:7701 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7721:7724 LamSF_Tactics <> rank def
R7710:7712 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7704:7707 LamSF_Tactics <> rank def
R7713:7716 LamSF_Tactics <> rank def
R7673:7701 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7721:7724 LamSF_Tactics <> rank def
R7710:7712 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7704:7707 LamSF_Tactics <> rank def
R7713:7716 LamSF_Tactics <> rank def
R7673:7701 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7721:7724 LamSF_Tactics <> rank def
R7710:7712 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7704:7707 LamSF_Tactics <> rank def
R7713:7716 LamSF_Tactics <> rank def
R7673:7701 Intensional_to_combinator <> to_combinator_int_rank_stable thm
R7721:7724 LamSF_Tactics <> rank def
R7710:7712 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7704:7707 LamSF_Tactics <> rank def
R7713:7716 LamSF_Tactics <> rank def
prf 7772:7806 <> to_combinator_int_makes_combinators
R7833:7836 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7837:7846 Combinators <> combinator ind
R7849:7865 Intensional_to_combinator <> to_combinator_int def
R7867:7867 Intensional_to_combinator <> M var
R7829:7831 Coq.Init.Logic <> :type_scope:x_'='_x not
R7821:7826 LamSF_Closed <> maxvar def
R7828:7828 Intensional_to_combinator <> M var
R7907:7911 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7924:7927 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7928:7937 Combinators <> combinator ind
R7940:7956 Intensional_to_combinator <> to_combinator_int def
R7958:7958 Intensional_to_combinator <> M var
R7920:7922 Coq.Init.Logic <> :type_scope:x_'='_x not
R7912:7917 LamSF_Closed <> maxvar def
R7919:7919 Intensional_to_combinator <> M var
R7897:7900 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7896:7896 Intensional_to_combinator <> p var
R7901:7904 LamSF_Tactics <> rank def
R7906:7906 Intensional_to_combinator <> M var
R7907:7911 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7924:7927 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7928:7937 Combinators <> combinator ind
R7940:7956 Intensional_to_combinator <> to_combinator_int def
R7958:7958 Intensional_to_combinator <> M var
R7920:7922 Coq.Init.Logic <> :type_scope:x_'='_x not
R7912:7917 LamSF_Closed <> maxvar def
R7919:7919 Intensional_to_combinator <> M var
R7897:7900 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R7896:7896 Intensional_to_combinator <> p var
R7901:7904 LamSF_Tactics <> rank def
R7906:7906 Intensional_to_combinator <> M var
R8023:8024 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8017:8020 LamSF_Tactics <> rank def
R8023:8024 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8017:8020 LamSF_Tactics <> rank def
R8039:8051 LamSF_Tactics <> rank_positive thm
R8133:8149 Intensional_to_combinator <> to_combinator_int def
R8152:8155 LamSF_Tactics <> rank def
R8158:8179 Intensional_to_combinator <> to_combinator_int_rank def
R8187:8208 Intensional_to_combinator <> to_combinator_int_rank def
R8187:8208 Intensional_to_combinator <> to_combinator_int_rank def
R8265:8268 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8261:8263 Coq.Init.Logic <> :type_scope:x_'='_x not
R8253:8258 LamSF_Closed <> maxvar def
R8277:8279 Coq.Init.Logic <> :type_scope:x_'='_x not
R8269:8274 LamSF_Closed <> maxvar def
R8265:8268 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8261:8263 Coq.Init.Logic <> :type_scope:x_'='_x not
R8253:8258 LamSF_Closed <> maxvar def
R8277:8279 Coq.Init.Logic <> :type_scope:x_'='_x not
R8269:8274 LamSF_Closed <> maxvar def
R8337:8359 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R8337:8359 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R8337:8359 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R8337:8359 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R8390:8397 Combinators <> comb_app constr
R8390:8397 Combinators <> comb_app constr
R8390:8397 Combinators <> comb_app constr
R8390:8397 Combinators <> comb_app constr
R8421:8425 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8447:8447 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8409:8418 Combinators <> combinator ind
R8438:8441 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8442:8446 Coq.Init.Logic <> False ind
R8426:8435 Combinators <> combinator ind
R8421:8425 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8447:8447 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R8409:8418 Combinators <> combinator ind
R8438:8441 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8442:8446 Coq.Init.Logic <> False ind
R8426:8435 Combinators <> combinator ind
R8461:8480 Combinators <> combinator_decidable thm
R8507:8532 Intensional_to_combinator <> to_combinator_int_app_comb thm
R8507:8532 Intensional_to_combinator <> to_combinator_int_app_comb thm
R8507:8532 Intensional_to_combinator <> to_combinator_int_app_comb thm
R8507:8532 Intensional_to_combinator <> to_combinator_int_app_comb thm
R8562:8569 Combinators <> comb_app constr
R8562:8569 Combinators <> comb_app constr
R8589:8596 Combinators <> comb_app constr
R8609:8638 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R8609:8638 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R8609:8638 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R8609:8638 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8657:8664 Combinators <> comb_app constr
R8751:8755 Coq.Init.Logic <> False ind
R8751:8755 Coq.Init.Logic <> False ind
R8816:8838 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R8816:8838 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R8816:8838 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R8816:8838 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R8869:8876 Combinators <> comb_app constr
R8869:8876 Combinators <> comb_app constr
R8869:8876 Combinators <> comb_app constr
R8869:8876 Combinators <> comb_app constr
R8915:8917 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8902:8905 LamSF_Tactics <> rank def
R8908:8911 SF_reduction <> star def
R8918:8921 LamSF_Tactics <> rank def
R8923:8925 LamSF_Terms <> Abs constr
R8915:8917 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8902:8905 LamSF_Tactics <> rank def
R8908:8911 SF_reduction <> star def
R8918:8921 LamSF_Tactics <> rank def
R8923:8925 LamSF_Terms <> Abs constr
R8942:8950 SF_reduction <> rank_star thm
R8982:8992 LamSF_Closed <> maxvar_star thm
R8982:8992 LamSF_Closed <> maxvar_star thm
R8982:8992 LamSF_Closed <> maxvar_star thm
R9070:9074 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9106:9106 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9048:9057 Combinators <> combinator ind
R9060:9062 LamSF_Terms <> App constr
R9097:9100 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9101:9105 Coq.Init.Logic <> False ind
R9075:9084 Combinators <> combinator ind
R9087:9089 LamSF_Terms <> App constr
R9070:9074 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9106:9106 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9048:9057 Combinators <> combinator ind
R9060:9062 LamSF_Terms <> App constr
R9097:9100 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9101:9105 Coq.Init.Logic <> False ind
R9075:9084 Combinators <> combinator ind
R9087:9089 LamSF_Terms <> App constr
R9120:9139 Combinators <> combinator_decidable thm
R9166:9191 Intensional_to_combinator <> to_combinator_int_app_comb thm
R9166:9191 Intensional_to_combinator <> to_combinator_int_app_comb thm
R9166:9191 Intensional_to_combinator <> to_combinator_int_app_comb thm
R9166:9191 Intensional_to_combinator <> to_combinator_int_app_comb thm
R9221:9228 Combinators <> comb_app constr
R9248:9277 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R9248:9277 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R9248:9277 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R9248:9277 Intensional_to_combinator <> to_combinator_int_app_not_comb thm
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
R9296:9303 Combinators <> comb_app constr
prf 9393:9424 <> to_combinator_int_is_extensional
R9451:9454 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9455:9465 Eta <> beta_eta_eq ind
R9470:9486 Intensional_to_combinator <> to_combinator_int def
R9488:9488 Intensional_to_combinator <> M var
R9467:9467 Intensional_to_combinator <> M var
R9447:9449 Coq.Init.Logic <> :type_scope:x_'='_x not
R9439:9444 LamSF_Closed <> maxvar def
R9446:9446 Intensional_to_combinator <> M var
R9528:9532 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9545:9548 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9549:9559 Eta <> beta_eta_eq ind
R9564:9580 Intensional_to_combinator <> to_combinator_int def
R9582:9582 Intensional_to_combinator <> M var
R9561:9561 Intensional_to_combinator <> M var
R9541:9543 Coq.Init.Logic <> :type_scope:x_'='_x not
R9533:9538 LamSF_Closed <> maxvar def
R9540:9540 Intensional_to_combinator <> M var
R9518:9521 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9517:9517 Intensional_to_combinator <> p var
R9522:9525 LamSF_Tactics <> rank def
R9527:9527 Intensional_to_combinator <> M var
R9528:9532 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9545:9548 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9549:9559 Eta <> beta_eta_eq ind
R9564:9580 Intensional_to_combinator <> to_combinator_int def
R9582:9582 Intensional_to_combinator <> M var
R9561:9561 Intensional_to_combinator <> M var
R9541:9543 Coq.Init.Logic <> :type_scope:x_'='_x not
R9533:9538 LamSF_Closed <> maxvar def
R9540:9540 Intensional_to_combinator <> M var
R9518:9521 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R9517:9517 Intensional_to_combinator <> p var
R9522:9525 LamSF_Tactics <> rank def
R9527:9527 Intensional_to_combinator <> M var
R9648:9649 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R9642:9645 LamSF_Tactics <> rank def
R9648:9649 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R9642:9645 LamSF_Tactics <> rank def
R9664:9676 LamSF_Tactics <> rank_positive thm
R9739:9742 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9735:9737 Coq.Init.Logic <> :type_scope:x_'='_x not
R9727:9732 LamSF_Closed <> maxvar def
R9751:9753 Coq.Init.Logic <> :type_scope:x_'='_x not
R9743:9748 LamSF_Closed <> maxvar def
R9739:9742 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R9735:9737 Coq.Init.Logic <> :type_scope:x_'='_x not
R9727:9732 LamSF_Closed <> maxvar def
R9751:9753 Coq.Init.Logic <> :type_scope:x_'='_x not
R9743:9748 LamSF_Closed <> maxvar def
R9811:9833 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R9811:9833 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R9811:9833 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R9811:9833 Intensional_to_combinator <> to_combinator_int_abs_0 thm
R9844:9854 Eta <> beta_eta_eq ind
R9901:9917 Intensional_to_combinator <> to_combinator_int def
R9919:9921 LamSF_Terms <> App constr
R9923:9926 SF_reduction <> k_op def
R9857:9863 Unstar <> abs_tag def
R9867:9883 Intensional_to_combinator <> to_combinator_int def
R9886:9888 LamSF_Terms <> App constr
R9890:9893 SF_reduction <> k_op def
R9844:9854 Eta <> beta_eta_eq ind
R9901:9917 Intensional_to_combinator <> to_combinator_int def
R9919:9921 LamSF_Terms <> App constr
R9923:9926 SF_reduction <> k_op def
R9857:9863 Unstar <> abs_tag def
R9867:9883 Intensional_to_combinator <> to_combinator_int def
R9886:9888 LamSF_Terms <> App constr
R9890:9893 SF_reduction <> k_op def
R9942:9948 Unstar <> tag_ext thm
R9959:9969 Eta <> beta_eta_eq ind
R10004:10006 LamSF_Terms <> App constr
R10008:10011 SF_reduction <> k_op def
R9972:9988 Intensional_to_combinator <> to_combinator_int def
R9990:9992 LamSF_Terms <> App constr
R9994:9997 SF_reduction <> k_op def
R9959:9969 Eta <> beta_eta_eq ind
R10004:10006 LamSF_Terms <> App constr
R10008:10011 SF_reduction <> k_op def
R9972:9988 Intensional_to_combinator <> to_combinator_int def
R9990:9992 LamSF_Terms <> App constr
R9994:9997 SF_reduction <> k_op def
R10027:10037 Eta <> symm_etared constr
R10076:10077 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R10070:10073 LamSF_Tactics <> rank def
R10076:10077 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R10070:10073 LamSF_Tactics <> rank def
R10092:10104 LamSF_Tactics <> rank_positive thm
R10123:10133 Eta <> beta_eta_eq ind
R10149:10151 LamSF_Terms <> Abs constr
R10154:10156 LamSF_Terms <> App constr
R10187:10189 LamSF_Terms <> Ref constr
R10159:10166 LamSF_Terms <> lift_rec def
R10169:10171 LamSF_Terms <> App constr
R10173:10176 SF_reduction <> k_op def
R10136:10138 LamSF_Terms <> App constr
R10140:10143 SF_reduction <> k_op def
R10123:10133 Eta <> beta_eta_eq ind
R10149:10151 LamSF_Terms <> Abs constr
R10154:10156 LamSF_Terms <> App constr
R10187:10189 LamSF_Terms <> Ref constr
R10159:10166 LamSF_Terms <> lift_rec def
R10169:10171 LamSF_Terms <> App constr
R10173:10176 SF_reduction <> k_op def
R10136:10138 LamSF_Terms <> App constr
R10140:10143 SF_reduction <> k_op def
R10228:10242 LamSF_Closed <> lift_rec_closed thm
R10228:10242 LamSF_Closed <> lift_rec_closed thm
R10228:10242 LamSF_Closed <> lift_rec_closed thm
R10228:10242 LamSF_Closed <> lift_rec_closed thm
R10272:10282 Eta <> beta_eta_eq ind
R10337:10339 LamSF_Terms <> Abs constr
R10285:10287 LamSF_Terms <> Abs constr
R10290:10292 LamSF_Terms <> App constr
R10327:10329 LamSF_Terms <> Ref constr
R10295:10297 LamSF_Terms <> App constr
R10300:10302 LamSF_Terms <> App constr
R10314:10315 LamSF_Terms <> Op constr
R10317:10319 LamSF_Terms <> Fop constr
R10305:10306 LamSF_Terms <> Op constr
R10308:10310 LamSF_Terms <> Fop constr
R10272:10282 Eta <> beta_eta_eq ind
R10337:10339 LamSF_Terms <> Abs constr
R10285:10287 LamSF_Terms <> Abs constr
R10290:10292 LamSF_Terms <> App constr
R10327:10329 LamSF_Terms <> Ref constr
R10295:10297 LamSF_Terms <> App constr
R10300:10302 LamSF_Terms <> App constr
R10314:10315 LamSF_Terms <> Op constr
R10317:10319 LamSF_Terms <> Fop constr
R10305:10306 LamSF_Terms <> Op constr
R10308:10310 LamSF_Terms <> Fop constr
R10395:10405 Eta <> beta_eta_eq ind
R10416:10418 LamSF_Terms <> Abs constr
R10408:10411 SF_reduction <> star def
R10395:10405 Eta <> beta_eta_eq ind
R10416:10418 LamSF_Terms <> Abs constr
R10408:10411 SF_reduction <> star def
R10435:10448 Eta <> star_equiv_abs thm
R10460:10482 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R10460:10482 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R10460:10482 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R10460:10482 Intensional_to_combinator <> to_combinator_int_abs_1 thm
R10493:10503 Eta <> beta_eta_eq ind
R10546:10562 Intensional_to_combinator <> to_combinator_int def
R10564:10567 SF_reduction <> star def
R10506:10512 Unstar <> abs_tag def
R10516:10532 Intensional_to_combinator <> to_combinator_int def
R10535:10538 SF_reduction <> star def
R10493:10503 Eta <> beta_eta_eq ind
R10546:10562 Intensional_to_combinator <> to_combinator_int def
R10564:10567 SF_reduction <> star def
R10506:10512 Unstar <> abs_tag def
R10516:10532 Intensional_to_combinator <> to_combinator_int def
R10535:10538 SF_reduction <> star def
R10583:10589 Unstar <> tag_ext thm
R10600:10610 Eta <> beta_eta_eq ind
R10641:10644 SF_reduction <> star def
R10613:10629 Intensional_to_combinator <> to_combinator_int def
R10631:10634 SF_reduction <> star def
R10600:10610 Eta <> beta_eta_eq ind
R10641:10644 SF_reduction <> star def
R10613:10629 Intensional_to_combinator <> to_combinator_int def
R10631:10634 SF_reduction <> star def
R10660:10670 Eta <> symm_etared constr
R10716:10718 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10703:10706 LamSF_Tactics <> rank def
R10709:10712 SF_reduction <> star def
R10719:10722 LamSF_Tactics <> rank def
R10725:10727 LamSF_Terms <> Abs constr
R10716:10718 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10703:10706 LamSF_Tactics <> rank def
R10709:10712 SF_reduction <> star def
R10719:10722 LamSF_Tactics <> rank def