forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Equal.glob
1126 lines (1126 loc) · 46.2 KB
/
Equal.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 02f6ce5937fd8c938db7740dd177e4ff
FEqual
R1993:2001 Coq.setoid_ring.ArithRing <> <> lib
R2019:2021 Coq.Arith.Max <> <> lib
R2040:2043 Test <> <> lib
R2061:2067 General <> <> lib
R2086:2096 LamSF_Terms <> <> lib
R2114:2126 LamSF_Tactics <> <> lib
R2144:2166 LamSF_Substitution_term <> <> lib
R2184:2195 SF_reduction <> <> lib
R2213:2227 LamSF_reduction <> <> lib
R2245:2256 LamSF_Normal <> <> lib
R2274:2285 LamSF_Closed <> <> lib
R2303:2312 LamSF_Eval <> <> lib
R2330:2334 Coq.omega.Omega <> <> lib
def 2376:2382 <> is_atom
R2392:2394 LamSF_Terms <> App constr
R2425:2427 LamSF_Terms <> App constr
R2435:2437 LamSF_Terms <> App constr
R2445:2447 LamSF_Terms <> App constr
R2454:2457 SF_reduction <> i_op def
R2449:2452 SF_reduction <> k_op def
R2439:2442 SF_reduction <> k_op def
R2429:2432 SF_reduction <> k_op def
R2397:2399 LamSF_Terms <> App constr
R2418:2421 SF_reduction <> k_op def
R2402:2404 LamSF_Terms <> App constr
R2415:2415 Equal <> M var
R2407:2408 LamSF_Terms <> Op constr
R2410:2412 LamSF_Terms <> Fop constr
def 2475:2481 <> S_not_F
R2488:2490 LamSF_Terms <> App constr
R2531:2534 SF_reduction <> i_op def
R2493:2495 LamSF_Terms <> App constr
R2525:2528 SF_reduction <> k_op def
R2498:2500 LamSF_Terms <> App constr
R2519:2522 SF_reduction <> k_op def
R2503:2505 LamSF_Terms <> App constr
R2510:2511 LamSF_Terms <> Op constr
R2513:2515 LamSF_Terms <> Fop constr
R2507:2507 Equal <> M var
prf 2544:2552 <> S_not_F_S
R2556:2564 LamSF_reduction <> lamSF_red def
R2585:2588 SF_reduction <> k_op def
R2567:2573 Equal <> S_not_F def
R2576:2577 LamSF_Terms <> Op constr
R2579:2581 LamSF_Terms <> Sop constr
R2606:2609 SF_reduction <> i_op def
R2612:2615 SF_reduction <> k_op def
R2618:2624 Equal <> S_not_F def
prf 2667:2675 <> S_not_F_F
R2679:2687 LamSF_reduction <> lamSF_red def
R2709:2711 LamSF_Terms <> App constr
R2718:2721 SF_reduction <> i_op def
R2713:2716 SF_reduction <> k_op def
R2690:2696 Equal <> S_not_F def
R2699:2700 LamSF_Terms <> Op constr
R2702:2704 LamSF_Terms <> Fop constr
R2740:2743 SF_reduction <> i_op def
R2746:2749 SF_reduction <> k_op def
R2752:2758 Equal <> S_not_F def
def 2806:2810 <> eq_op
R2819:2821 LamSF_Eval <> iff def
R2836:2842 Equal <> S_not_F def
R2844:2844 Equal <> N var
R2824:2830 Equal <> S_not_F def
R2832:2832 Equal <> M var
def 2860:2869 <> equal_body
R2981:2983 LamSF_Terms <> App constr
R3268:3270 LamSF_Terms <> Abs constr
R3273:3275 LamSF_Terms <> Abs constr
R3348:3350 LamSF_Terms <> App constr
R3484:3486 LamSF_Terms <> Abs constr
R3489:3491 LamSF_Terms <> Abs constr
R3516:3518 LamSF_Terms <> App constr
R3676:3678 LamSF_Terms <> App constr
R3685:3688 SF_reduction <> i_op def
R3680:3683 SF_reduction <> k_op def
R3520:3522 LamSF_Terms <> App constr
R3602:3604 LamSF_Terms <> App constr
R3625:3627 LamSF_Terms <> Ref constr
R3606:3608 LamSF_Terms <> App constr
R3617:3619 LamSF_Terms <> Ref constr
R3610:3612 LamSF_Terms <> Ref constr
R3524:3526 LamSF_Terms <> App constr
R3547:3549 LamSF_Terms <> Ref constr
R3528:3530 LamSF_Terms <> App constr
R3539:3541 LamSF_Terms <> Ref constr
R3532:3534 LamSF_Terms <> Ref constr
R3352:3354 LamSF_Terms <> App constr
R3420:3422 LamSF_Terms <> App constr
R3429:3432 SF_reduction <> i_op def
R3424:3427 SF_reduction <> k_op def
R3356:3358 LamSF_Terms <> App constr
R3370:3372 LamSF_Terms <> Ref constr
R3361:3362 LamSF_Terms <> Op constr
R3364:3366 LamSF_Terms <> Fop constr
R2985:2987 LamSF_Terms <> App constr
R3059:3061 LamSF_Terms <> App constr
R3209:3211 LamSF_Terms <> App constr
R3218:3220 LamSF_Terms <> App constr
R3227:3229 LamSF_Terms <> App constr
R3236:3239 SF_reduction <> i_op def
R3231:3234 SF_reduction <> k_op def
R3222:3225 SF_reduction <> k_op def
R3213:3216 SF_reduction <> k_op def
R3063:3065 LamSF_Terms <> App constr
R3145:3149 Equal <> eq_op def
R3160:3162 LamSF_Terms <> Ref constr
R3152:3154 LamSF_Terms <> Ref constr
R3067:3069 LamSF_Terms <> App constr
R3081:3083 LamSF_Terms <> Ref constr
R3072:3073 LamSF_Terms <> Op constr
R3075:3077 LamSF_Terms <> Fop constr
R2989:2991 LamSF_Terms <> App constr
R3003:3005 LamSF_Terms <> Ref constr
R2994:2995 LamSF_Terms <> Op constr
R2997:2999 LamSF_Terms <> Fop constr
def 3711:3718 <> equal_fn
R3723:3725 LamSF_Terms <> Abs constr
R3728:3730 LamSF_Terms <> Abs constr
R3733:3735 LamSF_Terms <> Abs constr
R3737:3746 Equal <> equal_body def
def 3763:3767 <> equal
R3773:3775 LamSF_Terms <> App constr
R3786:3793 Equal <> equal_fn def
R3777:3784 LamSF_Eval <> fixpoint def
prf 3803:3817 <> equal_fn_closed
R3835:3837 Coq.Init.Logic <> :type_scope:x_'='_x not
R3820:3825 LamSF_Closed <> maxvar def
R3827:3834 Equal <> equal_fn def
R3855:3862 Equal <> equal_fn def
prf 3889:3900 <> equal_closed
R3916:3918 Coq.Init.Logic <> :type_scope:x_'='_x not
R3904:3909 LamSF_Closed <> maxvar def
R3911:3915 Equal <> equal def
R3987:3991 Equal <> equal def
R4020:4027 Equal <> equal_fn def
R4042:4051 Equal <> equal_body def
R4062:4064 LamSF_Eval <> iff def
R4074:4076 LamSF_Eval <> not def
R4119:4122 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4123:4128 LamSF_Closed <> maxvar def
R4130:4134 Equal <> equal def
R4119:4122 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4123:4128 LamSF_Closed <> maxvar def
R4130:4134 Equal <> equal def
R4166:4169 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4170:4175 LamSF_Closed <> maxvar def
R4178:4180 LamSF_Terms <> App constr
R4191:4198 Equal <> equal_fn def
R4182:4189 LamSF_Eval <> fixpoint def
R4166:4169 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4170:4175 LamSF_Closed <> maxvar def
R4178:4180 LamSF_Terms <> App constr
R4191:4198 Equal <> equal_fn def
R4182:4189 LamSF_Eval <> fixpoint def
R4252:4255 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4256:4261 LamSF_Closed <> maxvar def
R4263:4270 LamSF_Eval <> fixpoint def
R4252:4255 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4256:4261 LamSF_Closed <> maxvar def
R4263:4270 LamSF_Eval <> fixpoint def
R4321:4324 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4325:4330 LamSF_Closed <> maxvar def
R4332:4339 Equal <> equal_fn def
R4321:4324 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R4325:4330 LamSF_Closed <> maxvar def
R4332:4339 Equal <> equal_fn def
R4352:4366 Equal <> equal_fn_closed thm
R4283:4297 LamSF_Eval <> fixpoint_closed thm
R4217:4228 Equal <> equal_closed thm
R4146:4150 Equal <> equal def
R4466:4475 LamSF_Terms <> insert_Ref def
prf 4496:4503 <> equal_op
R4517:4525 LamSF_reduction <> lamSF_red def
R4559:4562 SF_reduction <> k_op def
R4528:4530 LamSF_Terms <> App constr
R4552:4553 LamSF_Terms <> Op constr
R4555:4555 Equal <> o var
R4533:4535 LamSF_Terms <> App constr
R4544:4545 LamSF_Terms <> Op constr
R4547:4547 Equal <> o var
R4537:4541 Equal <> equal def
R4592:4596 Equal <> equal def
R4634:4636 LamSF_Terms <> App constr
R4691:4692 LamSF_Terms <> Op constr
R4639:4641 LamSF_Terms <> App constr
R4683:4684 LamSF_Terms <> Op constr
R4644:4646 LamSF_Terms <> App constr
R4658:4660 LamSF_Terms <> App constr
R4671:4678 Equal <> equal_fn def
R4662:4669 LamSF_Eval <> fixpoint def
R4648:4655 Equal <> equal_fn def
R4612:4625 LamSF_Tactics <> transitive_red thm
R4634:4636 LamSF_Terms <> App constr
R4691:4692 LamSF_Terms <> Op constr
R4639:4641 LamSF_Terms <> App constr
R4683:4684 LamSF_Terms <> Op constr
R4644:4646 LamSF_Terms <> App constr
R4658:4660 LamSF_Terms <> App constr
R4671:4678 Equal <> equal_fn def
R4662:4669 LamSF_Eval <> fixpoint def
R4648:4655 Equal <> equal_fn def
R4612:4625 LamSF_Tactics <> transitive_red thm
R4708:4730 LamSF_reduction <> preserves_app_lamSF_red thm
R4742:4764 LamSF_reduction <> preserves_app_lamSF_red thm
R4776:4780 LamSF_Eval <> fixes thm
R4791:4798 Equal <> equal_fn def
R4813:4822 Equal <> equal_body def
R4825:4827 LamSF_Eval <> iff def
R4830:4832 LamSF_Eval <> not def
R4854:4858 LamSF_Terms <> subst def
R4892:4895 LamSF_Terms <> lift def
R4906:4918 LamSF_Substitution_term <> lift_rec_null thm
R4906:4918 LamSF_Substitution_term <> lift_rec_null thm
R4906:4918 LamSF_Substitution_term <> lift_rec_null thm
prf 4981:4999 <> unequal_op_compound
R5026:5044 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5045:5053 LamSF_reduction <> lamSF_red def
R5083:5085 LamSF_Terms <> App constr
R5092:5095 SF_reduction <> i_op def
R5087:5090 SF_reduction <> k_op def
R5056:5058 LamSF_Terms <> App constr
R5079:5079 Equal <> M var
R5061:5063 LamSF_Terms <> App constr
R5072:5073 LamSF_Terms <> Op constr
R5075:5075 Equal <> o var
R5065:5069 Equal <> equal def
R5016:5023 SF_reduction <> compound ind
R5025:5025 Equal <> M var
R5147:5149 LamSF_Terms <> App constr
R5152:5154 LamSF_Terms <> App constr
R5196:5197 LamSF_Terms <> Op constr
R5157:5159 LamSF_Terms <> App constr
R5171:5173 LamSF_Terms <> App constr
R5184:5191 Equal <> equal_fn def
R5175:5182 LamSF_Eval <> fixpoint def
R5161:5168 Equal <> equal_fn def
R5125:5138 LamSF_Tactics <> transitive_red thm
R5147:5149 LamSF_Terms <> App constr
R5152:5154 LamSF_Terms <> App constr
R5196:5197 LamSF_Terms <> Op constr
R5157:5159 LamSF_Terms <> App constr
R5171:5173 LamSF_Terms <> App constr
R5184:5191 Equal <> equal_fn def
R5175:5182 LamSF_Eval <> fixpoint def
R5161:5168 Equal <> equal_fn def
R5125:5138 LamSF_Tactics <> transitive_red thm
R5216:5238 LamSF_reduction <> preserves_app_lamSF_red thm
R5250:5272 LamSF_reduction <> preserves_app_lamSF_red thm
R5284:5288 LamSF_Eval <> fixes thm
R5299:5306 Equal <> equal_fn def
R5321:5330 Equal <> equal_body def
R5366:5369 LamSF_Terms <> lift def
R5380:5392 LamSF_Substitution_term <> lift_rec_null thm
R5380:5392 LamSF_Substitution_term <> lift_rec_null thm
R5380:5392 LamSF_Substitution_term <> lift_rec_null thm
R5426:5435 LamSF_Tactics <> multi_step ind
R5449:5451 LamSF_Terms <> App constr
R5454:5456 LamSF_Terms <> App constr
R5459:5461 LamSF_Terms <> App constr
R5464:5465 LamSF_Terms <> Op constr
R5467:5469 LamSF_Terms <> Fop constr
R5437:5446 LamSF_reduction <> lamSF_red1 ind
R5426:5435 LamSF_Tactics <> multi_step ind
R5449:5451 LamSF_Terms <> App constr
R5454:5456 LamSF_Terms <> App constr
R5459:5461 LamSF_Terms <> App constr
R5464:5465 LamSF_Terms <> Op constr
R5467:5469 LamSF_Terms <> Fop constr
R5437:5446 LamSF_reduction <> lamSF_red1 ind
R5511:5513 LamSF_Terms <> App constr
R5543:5557 SF_reduction <> right_component def
R5516:5518 LamSF_Terms <> App constr
R5523:5536 SF_reduction <> left_component def
R5496:5503 LamSF_Tactics <> succ_red constr
R5511:5513 LamSF_Terms <> App constr
R5543:5557 SF_reduction <> right_component def
R5516:5518 LamSF_Terms <> App constr
R5523:5536 SF_reduction <> left_component def
R5496:5503 LamSF_Tactics <> succ_red constr
R5576:5595 LamSF_reduction <> f_compound_lamSF_red constr
prf 5625:5634 <> unequal_op
R5659:5662 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5675:5678 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5690:5708 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5709:5717 LamSF_reduction <> lamSF_red def
R5747:5749 LamSF_Terms <> App constr
R5756:5759 SF_reduction <> i_op def
R5751:5754 SF_reduction <> k_op def
R5720:5722 LamSF_Terms <> App constr
R5743:5743 Equal <> M var
R5725:5727 LamSF_Terms <> App constr
R5736:5737 LamSF_Terms <> Op constr
R5739:5739 Equal <> o var
R5729:5733 Equal <> equal def
R5680:5684 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R5689:5689 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R5679:5679 Equal <> M var
R5685:5686 LamSF_Terms <> Op constr
R5688:5688 Equal <> o var
R5671:5673 Coq.Init.Logic <> :type_scope:x_'='_x not
R5663:5668 LamSF_Closed <> maxvar def
R5670:5670 Equal <> M var
R5651:5656 LamSF_Normal <> normal ind
R5658:5658 Equal <> M var
R5790:5790 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5811:5815 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5791:5797 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5799:5800 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5802:5805 Coq.Init.Logic <> :type_scope:x_'='_x not
R5810:5810 Coq.Init.Logic <> :type_scope:x_'='_x not
R5806:5807 LamSF_Terms <> Op constr
R5809:5809 Equal <> o var
R5816:5823 SF_reduction <> compound ind
R5790:5790 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5811:5815 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5791:5797 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5799:5800 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5802:5805 Coq.Init.Logic <> :type_scope:x_'='_x not
R5810:5810 Coq.Init.Logic <> :type_scope:x_'='_x not
R5806:5807 LamSF_Terms <> Op constr
R5809:5809 Equal <> o var
R5816:5823 SF_reduction <> compound ind
R5838:5858 LamSF_Normal <> not_active_factorable thm
R5877:5880 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R5869:5874 LamSF_Tactics <> status def
R5881:5886 LamSF_Closed <> maxvar def
R5877:5880 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R5869:5874 LamSF_Tactics <> status def
R5881:5886 LamSF_Closed <> maxvar def
R5902:5917 LamSF_Closed <> status_lt_maxvar thm
R5955:5973 Equal <> unequal_op_compound thm
R6024:6026 LamSF_Terms <> App constr
R6081:6082 LamSF_Terms <> Op constr
R6029:6031 LamSF_Terms <> App constr
R6073:6074 LamSF_Terms <> Op constr
R6034:6036 LamSF_Terms <> App constr
R6048:6050 LamSF_Terms <> App constr
R6061:6068 Equal <> equal_fn def
R6052:6059 LamSF_Eval <> fixpoint def
R6038:6045 Equal <> equal_fn def
R6002:6015 LamSF_Tactics <> transitive_red thm
R6024:6026 LamSF_Terms <> App constr
R6081:6082 LamSF_Terms <> Op constr
R6029:6031 LamSF_Terms <> App constr
R6073:6074 LamSF_Terms <> Op constr
R6034:6036 LamSF_Terms <> App constr
R6048:6050 LamSF_Terms <> App constr
R6061:6068 Equal <> equal_fn def
R6052:6059 LamSF_Eval <> fixpoint def
R6038:6045 Equal <> equal_fn def
R6002:6015 LamSF_Tactics <> transitive_red thm
R6098:6120 LamSF_reduction <> preserves_app_lamSF_red thm
R6132:6154 LamSF_reduction <> preserves_app_lamSF_red thm
R6166:6170 LamSF_Eval <> fixes thm
R6181:6188 Equal <> equal_fn def
R6203:6212 Equal <> equal_body def
R6248:6251 LamSF_Terms <> lift def
R6262:6274 LamSF_Substitution_term <> lift_rec_null thm
R6262:6274 LamSF_Substitution_term <> lift_rec_null thm
R6262:6274 LamSF_Substitution_term <> lift_rec_null thm
prf 6358:6376 <> unequal_compound_op
R6403:6421 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6422:6430 LamSF_reduction <> lamSF_red def
R6459:6461 LamSF_Terms <> App constr
R6468:6471 SF_reduction <> i_op def
R6463:6466 SF_reduction <> k_op def
R6433:6435 LamSF_Terms <> App constr
R6452:6453 LamSF_Terms <> Op constr
R6455:6455 Equal <> o var
R6438:6440 LamSF_Terms <> App constr
R6448:6448 Equal <> M var
R6442:6446 Equal <> equal def
R6393:6400 SF_reduction <> compound ind
R6402:6402 Equal <> M var
R6522:6524 LamSF_Terms <> App constr
R6574:6575 LamSF_Terms <> Op constr
R6527:6529 LamSF_Terms <> App constr
R6532:6534 LamSF_Terms <> App constr
R6546:6548 LamSF_Terms <> App constr
R6559:6566 Equal <> equal_fn def
R6550:6557 LamSF_Eval <> fixpoint def
R6536:6543 Equal <> equal_fn def
R6500:6513 LamSF_Tactics <> transitive_red thm
R6522:6524 LamSF_Terms <> App constr
R6574:6575 LamSF_Terms <> Op constr
R6527:6529 LamSF_Terms <> App constr
R6532:6534 LamSF_Terms <> App constr
R6546:6548 LamSF_Terms <> App constr
R6559:6566 Equal <> equal_fn def
R6550:6557 LamSF_Eval <> fixpoint def
R6536:6543 Equal <> equal_fn def
R6500:6513 LamSF_Tactics <> transitive_red thm
R6591:6613 LamSF_reduction <> preserves_app_lamSF_red thm
R6625:6647 LamSF_reduction <> preserves_app_lamSF_red thm
R6659:6663 LamSF_Eval <> fixes thm
R6674:6681 Equal <> equal_fn def
R6696:6705 Equal <> equal_body def
R6729:6732 LamSF_Terms <> lift def
R6743:6755 LamSF_Substitution_term <> lift_rec_null thm
R6743:6755 LamSF_Substitution_term <> lift_rec_null thm
R6743:6755 LamSF_Substitution_term <> lift_rec_null thm
R6766:6783 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6766:6783 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6766:6783 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6766:6783 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6766:6783 LamSF_Substitution_term <> subst_rec_lift_rec thm
R6805:6817 LamSF_Substitution_term <> lift_rec_null thm
R6805:6817 LamSF_Substitution_term <> lift_rec_null thm
R6805:6817 LamSF_Substitution_term <> lift_rec_null thm
R6852:6861 LamSF_Tactics <> multi_step ind
R6875:6877 LamSF_Terms <> App constr
R6880:6882 LamSF_Terms <> App constr
R6885:6887 LamSF_Terms <> App constr
R6890:6891 LamSF_Terms <> Op constr
R6893:6895 LamSF_Terms <> Fop constr
R6863:6872 LamSF_reduction <> lamSF_red1 ind
R6852:6861 LamSF_Tactics <> multi_step ind
R6875:6877 LamSF_Terms <> App constr
R6880:6882 LamSF_Terms <> App constr
R6885:6887 LamSF_Terms <> App constr
R6890:6891 LamSF_Terms <> Op constr
R6893:6895 LamSF_Terms <> Fop constr
R6863:6872 LamSF_reduction <> lamSF_red1 ind
R6935:6937 LamSF_Terms <> App constr
R6967:6981 SF_reduction <> right_component def
R6940:6942 LamSF_Terms <> App constr
R6947:6960 SF_reduction <> left_component def
R6919:6926 LamSF_Tactics <> succ_red constr
R6935:6937 LamSF_Terms <> App constr
R6967:6981 SF_reduction <> right_component def
R6940:6942 LamSF_Terms <> App constr
R6947:6960 SF_reduction <> left_component def
R6919:6926 LamSF_Tactics <> succ_red constr
R7001:7020 LamSF_reduction <> f_compound_lamSF_red constr
prf 7062:7072 <> unequal_op2
R7097:7100 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7113:7116 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7128:7146 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7147:7155 LamSF_reduction <> lamSF_red def
R7184:7186 LamSF_Terms <> App constr
R7193:7196 SF_reduction <> i_op def
R7188:7191 SF_reduction <> k_op def
R7158:7160 LamSF_Terms <> App constr
R7177:7178 LamSF_Terms <> Op constr
R7180:7180 Equal <> o var
R7163:7165 LamSF_Terms <> App constr
R7173:7173 Equal <> M var
R7167:7171 Equal <> equal def
R7118:7122 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7127:7127 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R7117:7117 Equal <> M var
R7123:7124 LamSF_Terms <> Op constr
R7126:7126 Equal <> o var
R7109:7111 Coq.Init.Logic <> :type_scope:x_'='_x not
R7101:7106 LamSF_Closed <> maxvar def
R7108:7108 Equal <> M var
R7089:7094 LamSF_Normal <> normal ind
R7096:7096 Equal <> M var
R7226:7226 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7247:7251 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7227:7233 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7235:7236 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7238:7241 Coq.Init.Logic <> :type_scope:x_'='_x not
R7246:7246 Coq.Init.Logic <> :type_scope:x_'='_x not
R7242:7243 LamSF_Terms <> Op constr
R7245:7245 Equal <> o var
R7252:7259 SF_reduction <> compound ind
R7226:7226 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7247:7251 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7227:7233 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7235:7236 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7238:7241 Coq.Init.Logic <> :type_scope:x_'='_x not
R7246:7246 Coq.Init.Logic <> :type_scope:x_'='_x not
R7242:7243 LamSF_Terms <> Op constr
R7245:7245 Equal <> o var
R7252:7259 SF_reduction <> compound ind
R7274:7294 LamSF_Normal <> not_active_factorable thm
R7313:7316 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7305:7310 LamSF_Tactics <> status def
R7317:7322 LamSF_Closed <> maxvar def
R7313:7316 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7305:7310 LamSF_Tactics <> status def
R7317:7322 LamSF_Closed <> maxvar def
R7338:7353 LamSF_Closed <> status_lt_maxvar thm
R7391:7409 Equal <> unequal_compound_op thm
R7460:7462 LamSF_Terms <> App constr
R7517:7518 LamSF_Terms <> Op constr
R7465:7467 LamSF_Terms <> App constr
R7509:7510 LamSF_Terms <> Op constr
R7470:7472 LamSF_Terms <> App constr
R7484:7486 LamSF_Terms <> App constr
R7497:7504 Equal <> equal_fn def
R7488:7495 LamSF_Eval <> fixpoint def
R7474:7481 Equal <> equal_fn def
R7438:7451 LamSF_Tactics <> transitive_red thm
R7460:7462 LamSF_Terms <> App constr
R7517:7518 LamSF_Terms <> Op constr
R7465:7467 LamSF_Terms <> App constr
R7509:7510 LamSF_Terms <> Op constr
R7470:7472 LamSF_Terms <> App constr
R7484:7486 LamSF_Terms <> App constr
R7497:7504 Equal <> equal_fn def
R7488:7495 LamSF_Eval <> fixpoint def
R7474:7481 Equal <> equal_fn def
R7438:7451 LamSF_Tactics <> transitive_red thm
R7534:7556 LamSF_reduction <> preserves_app_lamSF_red thm
R7568:7590 LamSF_reduction <> preserves_app_lamSF_red thm
R7602:7606 LamSF_Eval <> fixes thm
R7617:7624 Equal <> equal_fn def
R7639:7648 Equal <> equal_body def
R7684:7687 LamSF_Terms <> lift def
R7698:7710 LamSF_Substitution_term <> lift_rec_null thm
R7698:7710 LamSF_Substitution_term <> lift_rec_null thm
R7698:7710 LamSF_Substitution_term <> lift_rec_null thm
R7842:7850 LamSF_reduction <> lamSF_red def
R7842:7850 LamSF_reduction <> lamSF_red def
R7883:7892 LamSF_Tactics <> multi_step ind
R7894:7903 LamSF_reduction <> lamSF_red1 ind
R7883:7892 LamSF_Tactics <> multi_step ind
R7894:7903 LamSF_reduction <> lamSF_red1 ind
R7943:7947 LamSF_Eval <> eval0 def
R7922:7935 LamSF_Tactics <> transitive_red thm
R7993:7997 LamSF_Eval <> eval0 def
R8000:8007 LamSF_Eval <> eval_app def
R8018:8022 LamSF_Terms <> subst def
R8032:8040 LamSF_Terms <> subst_rec def
R8048:8056 LamSF_Terms <> subst_rec def
R8064:8071 LamSF_Eval <> eval_app def
R8079:8083 LamSF_Eval <> eval0 def
prf 8115:8129 <> equal_compounds
R8156:8159 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8170:8174 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8175:8183 LamSF_reduction <> lamSF_red def
R8217:8219 LamSF_Terms <> App constr
R8432:8434 LamSF_Terms <> App constr
R8441:8444 SF_reduction <> i_op def
R8436:8439 SF_reduction <> k_op def
R8222:8224 LamSF_Terms <> App constr
R8338:8340 LamSF_Terms <> App constr
R8397:8411 SF_reduction <> right_component def
R8413:8413 Equal <> N var
R8343:8345 LamSF_Terms <> App constr
R8354:8368 SF_reduction <> right_component def
R8370:8370 Equal <> M var
R8347:8351 Equal <> equal def
R8244:8246 LamSF_Terms <> App constr
R8302:8315 SF_reduction <> left_component def
R8317:8317 Equal <> N var
R8249:8251 LamSF_Terms <> App constr
R8260:8273 SF_reduction <> left_component def
R8275:8275 Equal <> M var
R8253:8257 Equal <> equal def
R8186:8188 LamSF_Terms <> App constr
R8204:8204 Equal <> N var
R8191:8193 LamSF_Terms <> App constr
R8201:8201 Equal <> M var
R8195:8199 Equal <> equal def
R8160:8167 SF_reduction <> compound ind
R8169:8169 Equal <> N var
R8146:8153 SF_reduction <> compound ind
R8155:8155 Equal <> M var
R8497:8499 LamSF_Terms <> App constr
R8502:8504 LamSF_Terms <> App constr
R8507:8509 LamSF_Terms <> App constr
R8521:8523 LamSF_Terms <> App constr
R8534:8541 Equal <> equal_fn def
R8525:8532 LamSF_Eval <> fixpoint def
R8511:8518 Equal <> equal_fn def
R8475:8488 LamSF_Tactics <> transitive_red thm
R8497:8499 LamSF_Terms <> App constr
R8502:8504 LamSF_Terms <> App constr
R8507:8509 LamSF_Terms <> App constr
R8521:8523 LamSF_Terms <> App constr
R8534:8541 Equal <> equal_fn def
R8525:8532 LamSF_Eval <> fixpoint def
R8511:8518 Equal <> equal_fn def
R8475:8488 LamSF_Tactics <> transitive_red thm
R8571:8575 Equal <> equal def
R8586:8590 LamSF_Eval <> fixes thm
R8601:8608 Equal <> equal_fn def
R8623:8632 Equal <> equal_body def
R8640:8644 Equal <> equal def
R8640:8644 Equal <> equal def
R8706:8714 LamSF_Terms <> subst_rec def
R8722:8730 LamSF_Terms <> subst_rec def
R8722:8730 LamSF_Terms <> subst_rec def
R8759:8776 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8759:8776 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8759:8776 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8759:8776 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8759:8776 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8787:8799 LamSF_Substitution_term <> lift_rec_null thm
R8787:8799 LamSF_Substitution_term <> lift_rec_null thm
R8787:8799 LamSF_Substitution_term <> lift_rec_null thm
R8825:8834 LamSF_Tactics <> multi_step ind
R8848:8850 LamSF_Terms <> App constr
R8853:8855 LamSF_Terms <> App constr
R8858:8860 LamSF_Terms <> App constr
R8863:8864 LamSF_Terms <> Op constr
R8866:8868 LamSF_Terms <> Fop constr
R8836:8845 LamSF_reduction <> lamSF_red1 ind
R8825:8834 LamSF_Tactics <> multi_step ind
R8848:8850 LamSF_Terms <> App constr
R8853:8855 LamSF_Terms <> App constr
R8858:8860 LamSF_Terms <> App constr
R8863:8864 LamSF_Terms <> Op constr
R8866:8868 LamSF_Terms <> Fop constr
R8836:8845 LamSF_reduction <> lamSF_red1 ind
R8910:8912 LamSF_Terms <> App constr
R8942:8956 SF_reduction <> right_component def
R8915:8917 LamSF_Terms <> App constr
R8922:8935 SF_reduction <> left_component def
R8895:8902 LamSF_Tactics <> succ_red constr
R8910:8912 LamSF_Terms <> App constr
R8942:8956 SF_reduction <> right_component def
R8915:8917 LamSF_Terms <> App constr
R8922:8935 SF_reduction <> left_component def
R8895:8902 LamSF_Tactics <> succ_red constr
R9017:9034 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9017:9034 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9017:9034 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9017:9034 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9017:9034 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9046:9063 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9046:9063 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9046:9063 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9046:9063 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9046:9063 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9075:9087 LamSF_Substitution_term <> lift_rec_null thm
R9075:9087 LamSF_Substitution_term <> lift_rec_null thm
R9075:9087 LamSF_Substitution_term <> lift_rec_null thm
R9113:9122 LamSF_Tactics <> multi_step ind
R9136:9138 LamSF_Terms <> App constr
R9141:9143 LamSF_Terms <> App constr
R9146:9148 LamSF_Terms <> App constr
R9151:9152 LamSF_Terms <> Op constr
R9154:9156 LamSF_Terms <> Fop constr
R9124:9133 LamSF_reduction <> lamSF_red1 ind
R9113:9122 LamSF_Tactics <> multi_step ind
R9136:9138 LamSF_Terms <> App constr
R9141:9143 LamSF_Terms <> App constr
R9146:9148 LamSF_Terms <> App constr
R9151:9152 LamSF_Terms <> Op constr
R9154:9156 LamSF_Terms <> Fop constr
R9124:9133 LamSF_reduction <> lamSF_red1 ind
R9198:9200 LamSF_Terms <> App constr
R9230:9244 SF_reduction <> right_component def
R9203:9205 LamSF_Terms <> App constr
R9210:9223 SF_reduction <> left_component def
R9183:9190 LamSF_Tactics <> succ_red constr
R9198:9200 LamSF_Terms <> App constr
R9230:9244 SF_reduction <> right_component def
R9203:9205 LamSF_Terms <> App constr
R9210:9223 SF_reduction <> left_component def
R9183:9190 LamSF_Tactics <> succ_red constr
R9318:9326 LamSF_Terms <> subst_rec def
R9334:9342 LamSF_Terms <> subst_rec def
R9334:9342 LamSF_Terms <> subst_rec def
R9370:9378 LamSF_Terms <> subst_rec def
R9386:9394 LamSF_Terms <> subst_rec def
R9386:9394 LamSF_Terms <> subst_rec def
R9517:9534 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9517:9534 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9517:9534 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9517:9534 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9517:9534 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9569:9581 LamSF_Substitution_term <> lift_rec_null thm
R9569:9581 LamSF_Substitution_term <> lift_rec_null thm
R9569:9581 LamSF_Substitution_term <> lift_rec_null thm
R9569:9581 LamSF_Substitution_term <> lift_rec_null thm
R9591:9599 LamSF_reduction <> lamSF_red def
R9591:9599 LamSF_reduction <> lamSF_red def
R9623:9640 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9623:9640 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9623:9640 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9623:9640 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9623:9640 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9652:9669 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9652:9669 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9652:9669 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9652:9669 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9652:9669 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9681:9698 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9681:9698 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9681:9698 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9681:9698 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9681:9698 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9710:9722 LamSF_Substitution_term <> lift_rec_null thm
R9710:9722 LamSF_Substitution_term <> lift_rec_null thm
R9710:9722 LamSF_Substitution_term <> lift_rec_null thm
R9807:9824 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9807:9824 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9807:9824 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9807:9824 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9807:9824 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9836:9848 LamSF_Substitution_term <> lift_rec_null thm
R9836:9848 LamSF_Substitution_term <> lift_rec_null thm
R9836:9848 LamSF_Substitution_term <> lift_rec_null thm
R9889:9906 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9889:9906 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9889:9906 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9889:9906 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9889:9906 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9918:9935 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9918:9935 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9918:9935 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9918:9935 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9918:9935 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9947:9959 LamSF_Substitution_term <> lift_rec_null thm
R9947:9959 LamSF_Substitution_term <> lift_rec_null thm
R9947:9959 LamSF_Substitution_term <> lift_rec_null thm
prf 10031:10044 <> equal_programs
R10068:10071 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10072:10080 LamSF_reduction <> lamSF_red def
R10104:10107 SF_reduction <> k_op def
R10083:10085 LamSF_Terms <> App constr
R10101:10101 Equal <> M var
R10088:10090 LamSF_Terms <> App constr
R10098:10098 Equal <> M var
R10092:10096 Equal <> equal def
R10059:10065 LamSF_Closed <> program def
R10067:10067 Equal <> M var
R10146:10149 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10159:10163 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10164:10172 LamSF_reduction <> lamSF_red def
R10196:10199 SF_reduction <> k_op def
R10175:10177 LamSF_Terms <> App constr
R10193:10193 Equal <> M var
R10180:10182 LamSF_Terms <> App constr
R10190:10190 Equal <> M var
R10184:10188 Equal <> equal def
R10150:10156 LamSF_Closed <> program def
R10158:10158 Equal <> M var
R10136:10139 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R10135:10135 Equal <> p var
R10140:10143 LamSF_Tactics <> rank def
R10145:10145 Equal <> M var
R10146:10149 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10159:10163 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10164:10172 LamSF_reduction <> lamSF_red def
R10196:10199 SF_reduction <> k_op def
R10175:10177 LamSF_Terms <> App constr
R10193:10193 Equal <> M var
R10180:10182 LamSF_Terms <> App constr
R10190:10190 Equal <> M var
R10184:10188 Equal <> equal def
R10150:10156 LamSF_Closed <> program def
R10158:10158 Equal <> M var
R10136:10139 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R10135:10135 Equal <> p var
R10140:10143 LamSF_Tactics <> rank def
R10145:10145 Equal <> M var
R10211:10217 LamSF_Closed <> program def
R10281:10282 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R10275:10278 LamSF_Tactics <> rank def
R10281:10282 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R10275:10278 LamSF_Tactics <> rank def
R10297:10309 LamSF_Tactics <> rank_positive thm
R10339:10348 LamSF_Closed <> factorable def
R10339:10348 LamSF_Closed <> factorable def
R10363:10385 LamSF_Closed <> programs_are_factorable thm
R10431:10438 Equal <> equal_op thm
R10469:10471 LamSF_Terms <> App constr
R10609:10611 LamSF_Terms <> App constr
R10618:10621 SF_reduction <> i_op def
R10613:10616 SF_reduction <> k_op def
R10474:10476 LamSF_Terms <> App constr
R10545:10547 LamSF_Terms <> App constr
R10582:10596 SF_reduction <> right_component def
R10550:10552 LamSF_Terms <> App constr
R10561:10575 SF_reduction <> right_component def
R10554:10558 Equal <> equal def
R10479:10481 LamSF_Terms <> App constr
R10515:10528 SF_reduction <> left_component def
R10484:10486 LamSF_Terms <> App constr
R10495:10508 SF_reduction <> left_component def
R10488:10492 Equal <> equal def
R10447:10460 LamSF_Tactics <> transitive_red thm
R10469:10471 LamSF_Terms <> App constr
R10609:10611 LamSF_Terms <> App constr
R10618:10621 SF_reduction <> i_op def
R10613:10616 SF_reduction <> k_op def
R10474:10476 LamSF_Terms <> App constr
R10545:10547 LamSF_Terms <> App constr
R10582:10596 SF_reduction <> right_component def
R10550:10552 LamSF_Terms <> App constr
R10561:10575 SF_reduction <> right_component def
R10554:10558 Equal <> equal def
R10479:10481 LamSF_Terms <> App constr
R10515:10528 SF_reduction <> left_component def
R10484:10486 LamSF_Terms <> App constr
R10495:10508 SF_reduction <> left_component def
R10488:10492 Equal <> equal def
R10447:10460 LamSF_Tactics <> transitive_red thm
R10635:10649 Equal <> equal_compounds thm
R10681:10683 LamSF_Terms <> App constr
R10702:10704 LamSF_Terms <> App constr
R10711:10714 SF_reduction <> i_op def
R10706:10709 SF_reduction <> k_op def
R10686:10688 LamSF_Terms <> App constr
R10695:10698 SF_reduction <> k_op def
R10690:10693 SF_reduction <> k_op def
R10660:10673 LamSF_Tactics <> transitive_red thm
R10681:10683 LamSF_Terms <> App constr
R10702:10704 LamSF_Terms <> App constr
R10711:10714 SF_reduction <> i_op def
R10706:10709 SF_reduction <> k_op def
R10686:10688 LamSF_Terms <> App constr
R10695:10698 SF_reduction <> k_op def
R10690:10693 SF_reduction <> k_op def
R10660:10673 LamSF_Tactics <> transitive_red thm
R10727:10749 LamSF_reduction <> preserves_app_lamSF_red thm
R10761:10783 LamSF_reduction <> preserves_app_lamSF_red thm
R10844:10846 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10821:10824 LamSF_Tactics <> rank def
R10827:10840 SF_reduction <> left_component def
R10847:10850 LamSF_Tactics <> rank def
R10844:10846 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10821:10824 LamSF_Tactics <> rank def
R10827:10840 SF_reduction <> left_component def
R10847:10850 LamSF_Tactics <> rank def
R10866:10880 SF_reduction <> rank_compound_l thm
R10899:10905 LamSF_Closed <> program def
R10933:10950 LamSF_Normal <> normal_component_l thm
R10986:10989 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10961:10966 LamSF_Closed <> maxvar def
R10969:10982 SF_reduction <> left_component def
R10990:10995 LamSF_Closed <> maxvar def
R10986:10989 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10961:10966 LamSF_Closed <> maxvar def
R10969:10982 SF_reduction <> left_component def
R10990:10995 LamSF_Closed <> maxvar def
R11013:11043 LamSF_Closed <> left_component_preserves_maxvar thm
R11115:11117 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11091:11094 LamSF_Tactics <> rank def
R11097:11111 SF_reduction <> right_component def
R11118:11121 LamSF_Tactics <> rank def
R11115:11117 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11091:11094 LamSF_Tactics <> rank def
R11097:11111 SF_reduction <> right_component def
R11118:11121 LamSF_Tactics <> rank def
R11137:11151 SF_reduction <> rank_compound_r thm
R11170:11176 LamSF_Closed <> program def
R11204:11221 LamSF_Normal <> normal_component_r thm
R11258:11261 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11232:11237 LamSF_Closed <> maxvar def
R11240:11254 SF_reduction <> right_component def
R11262:11267 LamSF_Closed <> maxvar def
R11258:11261 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11232:11237 LamSF_Closed <> maxvar def
R11240:11254 SF_reduction <> right_component def
R11262:11267 LamSF_Closed <> maxvar def
R11285:11316 LamSF_Closed <> right_component_preserves_maxvar thm
prf 11380:11395 <> unequal_programs
R11421:11424 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11434:11437 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11442:11447 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11448:11456 LamSF_reduction <> lamSF_red def
R11481:11483 LamSF_Terms <> App constr
R11490:11493 SF_reduction <> i_op def
R11485:11488 SF_reduction <> k_op def
R11459:11461 LamSF_Terms <> App constr
R11477:11477 Equal <> N var
R11464:11466 LamSF_Terms <> App constr
R11474:11474 Equal <> M var
R11468:11472 Equal <> equal def
R11439:11440 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R11438:11438 Equal <> M var
R11441:11441 Equal <> N var
R11425:11431 LamSF_Closed <> program def
R11433:11433 Equal <> N var
R11412:11418 LamSF_Closed <> program def
R11420:11420 Equal <> M var
R11537:11540 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11550:11553 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11563:11566 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11571:11576 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11577:11585 LamSF_reduction <> lamSF_red def
R11610:11612 LamSF_Terms <> App constr
R11619:11622 SF_reduction <> i_op def
R11614:11617 SF_reduction <> k_op def
R11588:11590 LamSF_Terms <> App constr
R11606:11606 Equal <> N var
R11593:11595 LamSF_Terms <> App constr
R11603:11603 Equal <> M var
R11597:11601 Equal <> equal def
R11568:11569 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R11567:11567 Equal <> M var
R11570:11570 Equal <> N var
R11554:11560 LamSF_Closed <> program def
R11562:11562 Equal <> N var
R11541:11547 LamSF_Closed <> program def
R11549:11549 Equal <> M var
R11527:11530 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R11526:11526 Equal <> p var
R11531:11534 LamSF_Tactics <> rank def
R11536:11536 Equal <> M var
R11537:11540 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11550:11553 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11563:11566 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11571:11576 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11577:11585 LamSF_reduction <> lamSF_red def
R11610:11612 LamSF_Terms <> App constr
R11619:11622 SF_reduction <> i_op def
R11614:11617 SF_reduction <> k_op def
R11588:11590 LamSF_Terms <> App constr
R11606:11606 Equal <> N var
R11593:11595 LamSF_Terms <> App constr
R11603:11603 Equal <> M var
R11597:11601 Equal <> equal def
R11568:11569 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R11567:11567 Equal <> M var
R11570:11570 Equal <> N var
R11554:11560 LamSF_Closed <> program def
R11562:11562 Equal <> N var
R11541:11547 LamSF_Closed <> program def
R11549:11549 Equal <> M var
R11527:11530 Coq.Init.Peano <> :nat_scope:x_'>='_x not
R11526:11526 Equal <> p var
R11531:11534 LamSF_Tactics <> rank def
R11536:11536 Equal <> M var
R11690:11691 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R11684:11687 LamSF_Tactics <> rank def
R11690:11691 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R11684:11687 LamSF_Tactics <> rank def
R11706:11718 LamSF_Tactics <> rank_positive thm
R11748:11757 LamSF_Closed <> factorable def
R11748:11757 LamSF_Closed <> factorable def
R11773:11795 LamSF_Closed <> programs_are_factorable thm
R11807:11816 LamSF_Closed <> factorable def
R11807:11816 LamSF_Closed <> factorable def
R11832:11854 LamSF_Closed <> programs_are_factorable thm
R11866:11872 LamSF_Closed <> program def
R11937:11946 Equal <> unequal_op thm
R11957:11966 Equal <> unequal_op thm
R11977:11987 Equal <> unequal_op2 thm
R12040:12042 LamSF_Terms <> App constr
R12180:12182 LamSF_Terms <> App constr
R12189:12192 SF_reduction <> i_op def
R12184:12187 SF_reduction <> k_op def
R12045:12047 LamSF_Terms <> App constr
R12116:12118 LamSF_Terms <> App constr
R12153:12167 SF_reduction <> right_component def
R12121:12123 LamSF_Terms <> App constr
R12132:12146 SF_reduction <> right_component def
R12125:12129 Equal <> equal def
R12050:12052 LamSF_Terms <> App constr
R12086:12099 SF_reduction <> left_component def
R12055:12057 LamSF_Terms <> App constr
R12066:12079 SF_reduction <> left_component def
R12059:12063 Equal <> equal def
R12018:12031 LamSF_Tactics <> transitive_red thm
R12040:12042 LamSF_Terms <> App constr
R12180:12182 LamSF_Terms <> App constr
R12189:12192 SF_reduction <> i_op def
R12184:12187 SF_reduction <> k_op def
R12045:12047 LamSF_Terms <> App constr
R12116:12118 LamSF_Terms <> App constr
R12153:12167 SF_reduction <> right_component def
R12121:12123 LamSF_Terms <> App constr
R12132:12146 SF_reduction <> right_component def
R12125:12129 Equal <> equal def
R12050:12052 LamSF_Terms <> App constr
R12086:12099 SF_reduction <> left_component def
R12055:12057 LamSF_Terms <> App constr
R12066:12079 SF_reduction <> left_component def
R12059:12063 Equal <> equal def
R12018:12031 LamSF_Tactics <> transitive_red thm
R12206:12220 Equal <> equal_compounds thm
R12267:12270 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12248:12250 Coq.Init.Logic <> :type_scope:x_'='_x not
R12232:12245 SF_reduction <> left_component def
R12251:12264 SF_reduction <> left_component def
R12287:12290 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R12271:12284 SF_reduction <> left_component def
R12291:12304 SF_reduction <> left_component def
R12267:12270 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12248:12250 Coq.Init.Logic <> :type_scope:x_'='_x not
R12232:12245 SF_reduction <> left_component def
R12251:12264 SF_reduction <> left_component def
R12287:12290 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R12271:12284 SF_reduction <> left_component def
R12291:12304 SF_reduction <> left_component def
R12320:12342 LamSF_Terms <> decidable_term_equality thm
R12390:12393 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12370:12372 Coq.Init.Logic <> :type_scope:x_'='_x not
R12353:12367 SF_reduction <> right_component def
R12373:12387 SF_reduction <> right_component def
R12411:12414 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R12394:12408 SF_reduction <> right_component def
R12415:12429 SF_reduction <> right_component def
R12390:12393 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R12370:12372 Coq.Init.Logic <> :type_scope:x_'='_x not
R12353:12367 SF_reduction <> right_component def
R12373:12387 SF_reduction <> right_component def
R12411:12414 Coq.Init.Logic <> :type_scope:x_'<>'_x not
R12394:12408 SF_reduction <> right_component def