-
Notifications
You must be signed in to change notification settings - Fork 3
/
LamSF_Substitution.glob
989 lines (989 loc) · 42 KB
/
LamSF_Substitution.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
DIGEST ec4aaf6c13b024ce3b0192c39d78eb2d
FLamSF_Substitution
R2284:2288 Coq.Arith.Arith <> <> lib
R2306:2309 Test <> <> lib
R2327:2333 General <> <> lib
R2351:2361 LamSF_Terms <> <> lib
R2379:2401 LamSF_Substitution_term <> <> lib
R2419:2431 LamSF_Redexes <> <> lib
R2449:2453 Coq.omega.Omega <> <> lib
def 2598:2607 <> lift_rec_r
R2614:2620 LamSF_Redexes <> redexes ind
R2628:2631 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2635:2638 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2639:2645 LamSF_Redexes <> redexes ind
R2632:2634 Coq.Init.Datatypes <> nat ind
R2625:2627 Coq.Init.Datatypes <> nat ind
R2662:2664 Coq.Init.Datatypes <> nat ind
R2677:2677 LamSF_Substitution <> L var
R2688:2690 LamSF_Redexes <> Var constr
R2697:2699 LamSF_Redexes <> Var constr
R2702:2709 LamSF_Terms <> relocate def
R2715:2715 LamSF_Substitution <> n var
R2713:2713 LamSF_Substitution <> k var
R2722:2724 LamSF_Redexes <> Opp constr
R2731:2733 LamSF_Redexes <> Opp constr
R2741:2742 LamSF_Redexes <> Ap constr
R2753:2754 LamSF_Redexes <> Ap constr
R2778:2787 LamSF_Substitution <> lift_rec_r def
R2793:2793 LamSF_Substitution <> n var
R2791:2791 LamSF_Substitution <> k var
R2759:2768 LamSF_Substitution <> lift_rec_r def
R2774:2774 LamSF_Substitution <> n var
R2772:2772 LamSF_Substitution <> k var
R2800:2802 LamSF_Redexes <> Fun constr
R2809:2811 LamSF_Redexes <> Fun constr
R2814:2823 LamSF_Substitution <> lift_rec_r def
R2833:2833 LamSF_Substitution <> n var
R2828:2828 Coq.Init.Datatypes <> S constr
R2830:2830 LamSF_Substitution <> k var
def 2856:2861 <> lift_r
R2868:2870 Coq.Init.Datatypes <> nat ind
R2878:2884 LamSF_Redexes <> redexes ind
R2890:2899 LamSF_Substitution <> lift_rec_r def
R2905:2905 LamSF_Substitution <> n var
R2901:2901 LamSF_Substitution <> N var
def 2921:2930 <> insert_Var
R2937:2943 LamSF_Redexes <> redexes ind
R2953:2955 Coq.Init.Datatypes <> nat ind
R2969:2975 Test <> compare def
R2979:2979 LamSF_Substitution <> i var
R2977:2977 LamSF_Substitution <> k var
R3006:3011 Coq.Init.Specif <> inleft constr
R3014:3017 Coq.Init.Specif <> left constr
R3025:3027 LamSF_Redexes <> Var constr
R3030:3033 Coq.Init.Peano <> pred syndef
R3035:3035 LamSF_Substitution <> i var
R3053:3058 Coq.Init.Specif <> inleft constr
R3065:3070 LamSF_Substitution <> lift_r def
R3074:3074 LamSF_Substitution <> N var
R3072:3072 LamSF_Substitution <> k var
R3096:3098 LamSF_Redexes <> Var constr
R3100:3100 LamSF_Substitution <> i var
def 3156:3166 <> subst_rec_r
R3173:3179 LamSF_Redexes <> redexes ind
R3191:3194 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3198:3201 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3202:3208 LamSF_Redexes <> redexes ind
R3195:3197 Coq.Init.Datatypes <> nat ind
R3184:3190 LamSF_Redexes <> redexes ind
R3224:3230 LamSF_Redexes <> redexes ind
R3238:3240 Coq.Init.Datatypes <> nat ind
R3254:3254 LamSF_Substitution <> L var
R3265:3267 LamSF_Redexes <> Var constr
R3274:3283 LamSF_Substitution <> insert_Var def
R3289:3289 LamSF_Substitution <> k var
R3285:3285 LamSF_Substitution <> N var
R3295:3297 LamSF_Redexes <> Opp constr
R3304:3306 LamSF_Redexes <> Opp constr
R3314:3315 LamSF_Redexes <> Ap constr
R3327:3328 LamSF_Redexes <> Ap constr
R3353:3363 LamSF_Substitution <> subst_rec_r def
R3370:3370 LamSF_Substitution <> k var
R3368:3368 LamSF_Substitution <> N var
R3333:3343 LamSF_Substitution <> subst_rec_r def
R3349:3349 LamSF_Substitution <> k var
R3347:3347 LamSF_Substitution <> N var
R3377:3379 LamSF_Redexes <> Fun constr
R3386:3388 LamSF_Redexes <> Fun constr
R3391:3401 LamSF_Substitution <> subst_rec_r def
R3408:3408 Coq.Init.Datatypes <> S constr
R3410:3410 LamSF_Substitution <> k var
R3405:3405 LamSF_Substitution <> N var
def 3433:3439 <> subst_r
R3448:3454 LamSF_Redexes <> redexes ind
R3460:3470 LamSF_Substitution <> subst_rec_r def
R3474:3474 LamSF_Substitution <> N var
R3472:3472 LamSF_Substitution <> M var
prf 3509:3515 <> lift_le
R3536:3538 Coq.Init.Datatypes <> nat ind
R3548:3551 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3574:3576 Coq.Init.Logic <> :type_scope:x_'='_x not
R3552:3561 LamSF_Substitution <> lift_rec_r def
R3573:3573 LamSF_Substitution <> n var
R3571:3571 LamSF_Substitution <> k var
R3564:3566 LamSF_Redexes <> Var constr
R3568:3568 LamSF_Substitution <> i var
R3577:3579 LamSF_Redexes <> Var constr
R3583:3585 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3582:3582 LamSF_Substitution <> n var
R3586:3586 LamSF_Substitution <> i var
R3543:3546 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R3542:3542 LamSF_Substitution <> k var
R3547:3547 LamSF_Substitution <> i var
R3619:3626 LamSF_Terms <> relocate def
R3651:3654 Test <> test def
R3651:3654 Test <> test def
R3700:3702 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3700:3702 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R3733:3741 Coq.Arith.Gt <> le_not_gt thm
R3733:3741 Coq.Arith.Gt <> le_not_gt thm
prf 3776:3780 <> lift1
R3797:3803 LamSF_Redexes <> redexes ind
R3815:3817 Coq.Init.Datatypes <> nat ind
R3861:3863 Coq.Init.Logic <> :type_scope:x_'='_x not
R3822:3831 LamSF_Substitution <> lift_rec_r def
R3860:3860 LamSF_Substitution <> k var
R3854:3856 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3853:3853 LamSF_Substitution <> j var
R3857:3857 LamSF_Substitution <> i var
R3834:3843 LamSF_Substitution <> lift_rec_r def
R3849:3849 LamSF_Substitution <> j var
R3847:3847 LamSF_Substitution <> i var
R3845:3845 LamSF_Substitution <> U var
R3864:3873 LamSF_Substitution <> lift_rec_r def
R3881:3883 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3880:3880 LamSF_Substitution <> j var
R3884:3884 LamSF_Substitution <> k var
R3877:3877 LamSF_Substitution <> i var
R3875:3875 LamSF_Substitution <> U var
R3958:3965 LamSF_Terms <> relocate def
R3974:3977 Test <> test def
R3974:3977 Test <> test def
R4002:4005 Test <> test def
R4017:4019 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4009:4011 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4002:4005 Test <> test def
R4017:4019 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4009:4011 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4041:4052 Coq.Arith.Plus <> plus_permute syndef
R4060:4069 Coq.Arith.Plus <> plus_assoc syndef
R4041:4052 Coq.Arith.Plus <> plus_permute syndef
R4060:4069 Coq.Arith.Plus <> plus_assoc syndef
R4106:4109 Test <> test def
R4113:4115 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4106:4109 Test <> test def
R4113:4115 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4183:4183 Coq.Init.Datatypes <> S constr
R4186:4186 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4198:4199 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4200:4200 Coq.Init.Datatypes <> S constr
R4183:4183 Coq.Init.Datatypes <> S constr
R4186:4186 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4198:4199 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4200:4200 Coq.Init.Datatypes <> S constr
prf 4246:4258 <> lift_lift_rec
R4275:4281 LamSF_Redexes <> redexes ind
R4295:4297 Coq.Init.Datatypes <> nat ind
R4308:4312 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4352:4354 Coq.Init.Logic <> :type_scope:x_'='_x not
R4313:4322 LamSF_Substitution <> lift_rec_r def
R4351:4351 LamSF_Substitution <> k var
R4345:4347 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4344:4344 LamSF_Substitution <> p var
R4348:4348 LamSF_Substitution <> n var
R4325:4334 LamSF_Substitution <> lift_rec_r def
R4340:4340 LamSF_Substitution <> p var
R4338:4338 LamSF_Substitution <> i var
R4336:4336 LamSF_Substitution <> U var
R4355:4364 LamSF_Substitution <> lift_rec_r def
R4387:4387 LamSF_Substitution <> p var
R4385:4385 LamSF_Substitution <> i var
R4367:4376 LamSF_Substitution <> lift_rec_r def
R4382:4382 LamSF_Substitution <> k var
R4380:4380 LamSF_Substitution <> n var
R4378:4378 LamSF_Substitution <> U var
R4303:4306 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4302:4302 LamSF_Substitution <> i var
R4307:4307 LamSF_Substitution <> n var
R4483:4490 LamSF_Terms <> relocate def
R4507:4510 Test <> test def
R4525:4528 Test <> test def
R4507:4510 Test <> test def
R4525:4528 Test <> test def
R4525:4528 Test <> test def
R4557:4560 Test <> test def
R4573:4575 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4564:4566 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4587:4590 Test <> test def
R4596:4598 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4557:4560 Test <> test def
R4573:4575 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4564:4566 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4587:4590 Test <> test def
R4596:4598 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4587:4590 Test <> test def
R4596:4598 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4635:4646 Coq.Arith.Plus <> plus_permute syndef
R4635:4646 Coq.Arith.Plus <> plus_permute syndef
R4635:4646 Coq.Arith.Plus <> plus_permute syndef
R4678:4680 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4678:4680 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4727:4729 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4708:4718 Coq.Arith.Gt <> gt_le_trans thm
R4727:4729 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4708:4718 Coq.Arith.Gt <> gt_le_trans thm
R4764:4766 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4764:4766 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4794:4806 Coq.Arith.Gt <> plus_gt_reg_l thm
R4794:4806 Coq.Arith.Gt <> plus_gt_reg_l thm
R4846:4848 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4846:4848 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4876:4888 Coq.Arith.Gt <> plus_gt_reg_l thm
R4876:4888 Coq.Arith.Gt <> plus_gt_reg_l thm
R4935:4937 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4935:4937 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4968:4976 Coq.Arith.Gt <> le_not_gt thm
R4985:4992 Coq.Arith.Le <> le_trans syndef
R4968:4976 Coq.Arith.Gt <> le_not_gt thm
R4985:4992 Coq.Arith.Le <> le_trans syndef
R5037:5040 Test <> test def
R5053:5055 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5044:5046 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5037:5040 Test <> test def
R5053:5055 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5044:5046 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5115:5117 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5115:5117 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5148:5156 Coq.Arith.Gt <> le_not_gt thm
R5178:5180 Coq.Init.Datatypes <> nat ind
R5185:5197 Coq.Arith.Plus <> plus_le_reg_l thm
R5203:5203 LamSF_Substitution <> p var
R5201:5201 LamSF_Substitution <> m var
R5199:5199 LamSF_Substitution <> n var
R5148:5156 Coq.Arith.Gt <> le_not_gt thm
R5178:5180 Coq.Init.Datatypes <> nat ind
R5185:5197 Coq.Arith.Plus <> plus_le_reg_l thm
R5203:5203 LamSF_Substitution <> p var
R5201:5201 LamSF_Substitution <> m var
R5199:5199 LamSF_Substitution <> n var
R5249:5252 Test <> test def
R5256:5258 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5249:5252 Test <> test def
R5256:5258 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5320:5322 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5320:5322 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5353:5361 Coq.Arith.Gt <> le_not_gt thm
R5386:5388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5370:5377 Coq.Arith.Le <> le_trans syndef
R5353:5361 Coq.Arith.Gt <> le_not_gt thm
R5386:5388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5370:5377 Coq.Arith.Le <> le_trans syndef
R5571:5571 Coq.Init.Datatypes <> S constr
R5574:5576 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5588:5590 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5591:5591 Coq.Init.Datatypes <> S constr
R5571:5571 Coq.Init.Datatypes <> S constr
R5574:5576 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5588:5590 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5591:5591 Coq.Init.Datatypes <> S constr
prf 5645:5653 <> lift_lift
R5670:5676 LamSF_Redexes <> redexes ind
R5688:5690 Coq.Init.Datatypes <> nat ind
R5728:5730 Coq.Init.Logic <> :type_scope:x_'='_x not
R5695:5704 LamSF_Substitution <> lift_rec_r def
R5727:5727 LamSF_Substitution <> k var
R5721:5723 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5720:5720 LamSF_Substitution <> p var
R5724:5724 LamSF_Substitution <> n var
R5707:5712 LamSF_Substitution <> lift_r def
R5716:5716 LamSF_Substitution <> U var
R5714:5714 LamSF_Substitution <> p var
R5731:5736 LamSF_Substitution <> lift_r def
R5741:5750 LamSF_Substitution <> lift_rec_r def
R5756:5756 LamSF_Substitution <> k var
R5754:5754 LamSF_Substitution <> n var
R5752:5752 LamSF_Substitution <> U var
R5738:5738 LamSF_Substitution <> p var
R5774:5779 LamSF_Substitution <> lift_r def
R5804:5816 LamSF_Substitution <> lift_lift_rec thm
R5804:5816 LamSF_Substitution <> lift_lift_rec thm
prf 6132:6148 <> lift_rec_lift_rec
R6165:6171 LamSF_Redexes <> redexes ind
R6185:6187 Coq.Init.Datatypes <> nat ind
R6202:6206 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6213:6216 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6250:6252 Coq.Init.Logic <> :type_scope:x_'='_x not
R6217:6226 LamSF_Substitution <> lift_rec_r def
R6249:6249 LamSF_Substitution <> p var
R6247:6247 LamSF_Substitution <> k var
R6229:6238 LamSF_Substitution <> lift_rec_r def
R6244:6244 LamSF_Substitution <> n var
R6242:6242 LamSF_Substitution <> i var
R6240:6240 LamSF_Substitution <> U var
R6253:6262 LamSF_Substitution <> lift_rec_r def
R6270:6272 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6269:6269 LamSF_Substitution <> p var
R6273:6273 LamSF_Substitution <> n var
R6266:6266 LamSF_Substitution <> i var
R6264:6264 LamSF_Substitution <> U var
R6208:6211 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6207:6207 LamSF_Substitution <> i var
R6212:6212 LamSF_Substitution <> k var
R6193:6196 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6192:6192 LamSF_Substitution <> k var
R6198:6200 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6197:6197 LamSF_Substitution <> i var
R6201:6201 LamSF_Substitution <> n var
R6355:6362 LamSF_Terms <> relocate def
R6379:6382 Test <> test def
R6379:6382 Test <> test def
R6405:6408 Test <> test def
R6415:6417 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6405:6408 Test <> test def
R6415:6417 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6440:6457 Coq.Arith.Plus <> plus_assoc_reverse thm
R6440:6457 Coq.Arith.Plus <> plus_assoc_reverse thm
R6440:6457 Coq.Arith.Plus <> plus_assoc_reverse thm
R6489:6491 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6494:6496 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6489:6491 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6494:6496 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6527:6535 Coq.Arith.Gt <> le_not_gt thm
R6560:6562 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6544:6551 Coq.Arith.Le <> le_trans syndef
R6527:6535 Coq.Arith.Gt <> le_not_gt thm
R6560:6562 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6544:6551 Coq.Arith.Le <> le_trans syndef
R6598:6600 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6613:6615 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6643:6658 Coq.Arith.Plus <> plus_le_compat_l thm
R6598:6600 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6613:6615 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6688:6691 Test <> test def
R6688:6691 Test <> test def
R6737:6739 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6737:6739 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6750:6758 Coq.Arith.Gt <> le_not_gt thm
R6750:6758 Coq.Arith.Gt <> le_not_gt thm
R6787:6797 Coq.Arith.Gt <> gt_le_trans thm
R6787:6797 Coq.Arith.Gt <> gt_le_trans thm
prf 6966:6978 <> lift_rec_lift
R6995:7001 LamSF_Redexes <> redexes ind
R7015:7017 Coq.Init.Datatypes <> nat ind
R7028:7031 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7059:7061 Coq.Init.Logic <> :type_scope:x_'='_x not
R7032:7041 LamSF_Substitution <> lift_rec_r def
R7058:7058 LamSF_Substitution <> p var
R7056:7056 LamSF_Substitution <> k var
R7044:7049 LamSF_Substitution <> lift_r def
R7053:7053 LamSF_Substitution <> U var
R7051:7051 LamSF_Substitution <> n var
R7062:7067 LamSF_Substitution <> lift_r def
R7077:7077 LamSF_Substitution <> U var
R7071:7073 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7070:7070 LamSF_Substitution <> p var
R7074:7074 LamSF_Substitution <> n var
R7023:7026 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7022:7022 LamSF_Substitution <> k var
R7027:7027 LamSF_Substitution <> n var
R7094:7099 LamSF_Substitution <> lift_r def
R7126:7142 LamSF_Substitution <> lift_rec_lift_rec thm
R7126:7142 LamSF_Substitution <> lift_rec_lift_rec thm
R7126:7142 LamSF_Substitution <> lift_rec_lift_rec thm
R7126:7142 LamSF_Substitution <> lift_rec_lift_rec thm
R7126:7142 LamSF_Substitution <> lift_rec_lift_rec thm
prf 7234:7241 <> subst_eq
R7260:7266 LamSF_Redexes <> redexes ind
R7274:7276 Coq.Init.Datatypes <> nat ind
R7306:7308 Coq.Init.Logic <> :type_scope:x_'='_x not
R7283:7293 LamSF_Substitution <> subst_rec_r def
R7305:7305 LamSF_Substitution <> n var
R7303:7303 LamSF_Substitution <> U var
R7296:7298 LamSF_Redexes <> Var constr
R7300:7300 LamSF_Substitution <> n var
R7309:7314 LamSF_Substitution <> lift_r def
R7318:7318 LamSF_Substitution <> U var
R7316:7316 LamSF_Substitution <> n var
R7350:7359 LamSF_Substitution <> insert_Var def
R7384:7390 Test <> compare def
R7384:7390 Test <> compare def
R7468:7470 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7468:7470 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7504:7506 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7504:7506 Coq.Init.Peano <> :nat_scope:x_'>'_x not
prf 7543:7550 <> subst_gt
R7569:7575 LamSF_Redexes <> redexes ind
R7585:7587 Coq.Init.Datatypes <> nat ind
R7597:7600 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7624:7627 Coq.Init.Logic <> :type_scope:x_'='_x not
R7601:7611 LamSF_Substitution <> subst_rec_r def
R7623:7623 LamSF_Substitution <> p var
R7621:7621 LamSF_Substitution <> U var
R7614:7616 LamSF_Redexes <> Var constr
R7618:7618 LamSF_Substitution <> n var
R7628:7630 LamSF_Redexes <> Var constr
R7633:7636 Coq.Init.Peano <> pred syndef
R7638:7638 LamSF_Substitution <> n var
R7593:7595 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7592:7592 LamSF_Substitution <> n var
R7596:7596 LamSF_Substitution <> p var
R7671:7680 LamSF_Substitution <> insert_Var def
R7705:7711 Test <> compare def
R7705:7711 Test <> compare def
R7774:7776 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7774:7776 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7841:7843 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7841:7843 Coq.Init.Peano <> :nat_scope:x_'>'_x not
prf 7878:7885 <> subst_lt
R7902:7908 LamSF_Redexes <> redexes ind
R7918:7920 Coq.Init.Datatypes <> nat ind
R7929:7932 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7956:7958 Coq.Init.Logic <> :type_scope:x_'='_x not
R7933:7943 LamSF_Substitution <> subst_rec_r def
R7955:7955 LamSF_Substitution <> p var
R7953:7953 LamSF_Substitution <> U var
R7946:7948 LamSF_Redexes <> Var constr
R7950:7950 LamSF_Substitution <> n var
R7959:7961 LamSF_Redexes <> Var constr
R7963:7963 LamSF_Substitution <> n var
R7925:7927 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7924:7924 LamSF_Substitution <> p var
R7928:7928 LamSF_Substitution <> n var
R7995:8004 LamSF_Substitution <> insert_Var def
R8029:8035 Test <> compare def
R8029:8035 Test <> compare def
R8081:8083 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8081:8083 Coq.Init.Peano <> :nat_scope:x_'>'_x not
prf 8212:8229 <> lift_rec_subst_rec
R8248:8254 LamSF_Redexes <> redexes ind
R8266:8268 Coq.Init.Datatypes <> nat ind
R8313:8316 Coq.Init.Logic <> :type_scope:x_'='_x not
R8273:8282 LamSF_Substitution <> lift_rec_r def
R8312:8312 LamSF_Substitution <> k var
R8306:8308 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8305:8305 LamSF_Substitution <> p var
R8309:8309 LamSF_Substitution <> n var
R8285:8295 LamSF_Substitution <> subst_rec_r def
R8301:8301 LamSF_Substitution <> p var
R8299:8299 LamSF_Substitution <> U var
R8297:8297 LamSF_Substitution <> V var
R8317:8327 LamSF_Substitution <> subst_rec_r def
R8377:8377 LamSF_Substitution <> p var
R8359:8368 LamSF_Substitution <> lift_rec_r def
R8374:8374 LamSF_Substitution <> k var
R8372:8372 LamSF_Substitution <> n var
R8370:8370 LamSF_Substitution <> U var
R8330:8339 LamSF_Substitution <> lift_rec_r def
R8355:8355 LamSF_Substitution <> k var
R8344:8344 Coq.Init.Datatypes <> S constr
R8348:8350 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8347:8347 LamSF_Substitution <> p var
R8351:8351 LamSF_Substitution <> n var
R8341:8341 LamSF_Substitution <> V var
R8443:8443 Coq.Init.Datatypes <> S constr
R8446:8448 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8462:8465 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8459:8459 Coq.Init.Datatypes <> S constr
R8443:8443 Coq.Init.Datatypes <> S constr
R8446:8448 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8462:8465 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8459:8459 Coq.Init.Datatypes <> S constr
R8517:8526 LamSF_Substitution <> insert_Var def
R8529:8536 LamSF_Terms <> relocate def
R8553:8559 Test <> compare def
R8553:8559 Test <> compare def
R8658:8661 Test <> test def
R8664:8664 Coq.Init.Datatypes <> S constr
R8668:8670 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8658:8661 Test <> test def
R8664:8664 Coq.Init.Datatypes <> S constr
R8668:8670 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8736:8742 Test <> compare def
R8748:8750 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8736:8742 Test <> compare def
R8748:8750 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8901:8908 LamSF_Terms <> relocate def
R8925:8928 Test <> test def
R8940:8943 Coq.Init.Peano <> pred syndef
R8932:8934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8925:8928 Test <> test def
R8940:8943 Coq.Init.Peano <> pred syndef
R8932:8934 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8975:8977 Coq.Init.Logic <> :type_scope:x_'='_x not
R8967:8968 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8969:8972 Coq.Init.Peano <> pred syndef
R8978:8981 Coq.Init.Peano <> pred syndef
R8985:8985 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8975:8977 Coq.Init.Logic <> :type_scope:x_'='_x not
R8967:8968 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8969:8972 Coq.Init.Peano <> pred syndef
R8978:8981 Coq.Init.Peano <> pred syndef
R8985:8985 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9049:9055 Test <> compare def
R9049:9055 Test <> compare def
R9143:9150 LamSF_Terms <> relocate def
R9193:9196 Test <> test def
R9208:9211 Coq.Init.Peano <> pred syndef
R9200:9202 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9193:9196 Test <> test def
R9208:9211 Coq.Init.Peano <> pred syndef
R9200:9202 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9264:9267 Test <> test def
R9270:9270 Coq.Init.Datatypes <> S constr
R9274:9276 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9264:9267 Test <> test def
R9270:9270 Coq.Init.Datatypes <> S constr
R9274:9276 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9401:9407 Test <> compare def
R9401:9407 Test <> compare def
R9497:9505 LamSF_Substitution <> lift_lift thm
R9497:9505 LamSF_Substitution <> lift_lift thm
R9497:9505 LamSF_Substitution <> lift_lift thm
R9566:9569 Test <> test def
R9572:9572 Coq.Init.Datatypes <> S constr
R9576:9578 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9566:9569 Test <> test def
R9572:9572 Coq.Init.Datatypes <> S constr
R9576:9578 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9651:9657 Test <> compare def
R9651:9657 Test <> compare def
R9755:9762 LamSF_Terms <> relocate def
R9771:9774 Test <> test def
R9778:9778 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9771:9774 Test <> test def
R9778:9778 Coq.Init.Peano <> :nat_scope:x_'+'_x not
prf 9823:9832 <> lift_subst
R9851:9857 LamSF_Redexes <> redexes ind
R9867:9869 Coq.Init.Datatypes <> nat ind
R9902:9905 Coq.Init.Logic <> :type_scope:x_'='_x not
R9874:9883 LamSF_Substitution <> lift_rec_r def
R9901:9901 LamSF_Substitution <> k var
R9899:9899 LamSF_Substitution <> n var
R9886:9892 LamSF_Substitution <> subst_r def
R9896:9896 LamSF_Substitution <> V var
R9894:9894 LamSF_Substitution <> U var
R9906:9912 LamSF_Substitution <> subst_r def
R9934:9943 LamSF_Substitution <> lift_rec_r def
R9953:9953 LamSF_Substitution <> k var
R9948:9948 Coq.Init.Datatypes <> S constr
R9950:9950 LamSF_Substitution <> n var
R9945:9945 LamSF_Substitution <> V var
R9915:9924 LamSF_Substitution <> lift_rec_r def
R9930:9930 LamSF_Substitution <> k var
R9928:9928 LamSF_Substitution <> n var
R9926:9926 LamSF_Substitution <> U var
R9971:9977 LamSF_Substitution <> subst_r def
R10005:10005 Coq.Init.Datatypes <> S constr
R10016:10016 Coq.Init.Datatypes <> S constr
R10020:10022 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10005:10005 Coq.Init.Datatypes <> S constr
R10016:10016 Coq.Init.Datatypes <> S constr
R10020:10022 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10033:10050 LamSF_Substitution <> lift_rec_subst_rec thm
R10033:10050 LamSF_Substitution <> lift_rec_subst_rec thm
prf 10121:10139 <> subst_rec_lift_rec1
R10158:10164 LamSF_Redexes <> redexes ind
R10176:10178 Coq.Init.Datatypes <> nat ind
R10189:10193 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10234:10237 Coq.Init.Logic <> :type_scope:x_'='_x not
R10194:10204 LamSF_Substitution <> subst_rec_r def
R10229:10231 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10228:10228 LamSF_Substitution <> p var
R10232:10232 LamSF_Substitution <> n var
R10225:10225 LamSF_Substitution <> V var
R10207:10216 LamSF_Substitution <> lift_rec_r def
R10222:10222 LamSF_Substitution <> p var
R10220:10220 LamSF_Substitution <> k var
R10218:10218 LamSF_Substitution <> U var
R10238:10247 LamSF_Substitution <> lift_rec_r def
R10271:10271 LamSF_Substitution <> p var
R10269:10269 LamSF_Substitution <> k var
R10250:10260 LamSF_Substitution <> subst_rec_r def
R10266:10266 LamSF_Substitution <> n var
R10264:10264 LamSF_Substitution <> V var
R10262:10262 LamSF_Substitution <> U var
R10184:10187 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R10183:10183 LamSF_Substitution <> k var
R10188:10188 LamSF_Substitution <> n var
R10352:10359 LamSF_Terms <> relocate def
R10368:10371 Test <> test def
R10368:10371 Test <> test def
R10410:10419 LamSF_Substitution <> insert_Var def
R10428:10434 Test <> compare def
R10445:10445 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10438:10438 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10456:10462 Test <> compare def
R10428:10434 Test <> compare def
R10445:10445 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10438:10438 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10456:10462 Test <> compare def
R10456:10462 Test <> compare def
R10565:10572 LamSF_Terms <> relocate def
R10581:10584 Test <> test def
R10589:10592 Coq.Init.Peano <> pred syndef
R10581:10584 Test <> test def
R10589:10592 Coq.Init.Peano <> pred syndef
R10639:10641 Coq.Init.Logic <> :type_scope:x_'='_x not
R10629:10632 Coq.Init.Peano <> pred syndef
R10636:10636 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10643:10645 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10646:10649 Coq.Init.Peano <> pred syndef
R10639:10641 Coq.Init.Logic <> :type_scope:x_'='_x not
R10629:10632 Coq.Init.Peano <> pred syndef
R10636:10636 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10643:10645 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10646:10649 Coq.Init.Peano <> pred syndef
R10729:10741 LamSF_Substitution <> lift_rec_lift thm
R10729:10741 LamSF_Substitution <> lift_rec_lift thm
R10729:10741 LamSF_Substitution <> lift_rec_lift thm
R10729:10741 LamSF_Substitution <> lift_rec_lift thm
R10729:10741 LamSF_Substitution <> lift_rec_lift thm
R10827:10834 LamSF_Terms <> relocate def
R10843:10846 Test <> test def
R10843:10846 Test <> test def
R10885:10894 LamSF_Substitution <> insert_Var def
R10903:10909 Test <> compare def
R10903:10909 Test <> compare def
R10977:10983 Test <> compare def
R10987:10987 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10977:10983 Test <> compare def
R10987:10987 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11057:11064 LamSF_Terms <> relocate def
R11073:11076 Test <> test def
R11073:11076 Test <> test def
R11164:11164 Coq.Init.Datatypes <> S constr
R11167:11169 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11181:11184 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11188:11188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11185:11185 Coq.Init.Datatypes <> S constr
R11164:11164 Coq.Init.Datatypes <> S constr
R11167:11169 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11181:11184 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11188:11188 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11185:11185 Coq.Init.Datatypes <> S constr
prf 11245:11259 <> subst_rec_lift1
R11278:11284 LamSF_Redexes <> redexes ind
R11294:11296 Coq.Init.Datatypes <> nat ind
R11335:11337 Coq.Init.Logic <> :type_scope:x_'='_x not
R11301:11311 LamSF_Substitution <> subst_rec_r def
R11330:11332 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11329:11329 LamSF_Substitution <> p var
R11333:11333 LamSF_Substitution <> n var
R11326:11326 LamSF_Substitution <> V var
R11314:11319 LamSF_Substitution <> lift_r def
R11323:11323 LamSF_Substitution <> U var
R11321:11321 LamSF_Substitution <> p var
R11338:11343 LamSF_Substitution <> lift_r def
R11348:11358 LamSF_Substitution <> subst_rec_r def
R11364:11364 LamSF_Substitution <> n var
R11362:11362 LamSF_Substitution <> V var
R11360:11360 LamSF_Substitution <> U var
R11345:11345 LamSF_Substitution <> p var
R11382:11387 LamSF_Substitution <> lift_r def
R11414:11432 LamSF_Substitution <> subst_rec_lift_rec1 thm
R11414:11432 LamSF_Substitution <> subst_rec_lift_rec1 thm
R11414:11432 LamSF_Substitution <> subst_rec_lift_rec1 thm
R11414:11432 LamSF_Substitution <> subst_rec_lift_rec1 thm
prf 11469:11486 <> subst_rec_lift_rec
R11505:11511 LamSF_Redexes <> redexes ind
R11523:11525 Coq.Init.Datatypes <> nat ind
R11540:11544 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11551:11554 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11593:11595 Coq.Init.Logic <> :type_scope:x_'='_x not
R11555:11565 LamSF_Substitution <> subst_rec_r def
R11592:11592 LamSF_Substitution <> q var
R11590:11590 LamSF_Substitution <> V var
R11568:11577 LamSF_Substitution <> lift_rec_r def
R11584:11584 Coq.Init.Datatypes <> S constr
R11586:11586 LamSF_Substitution <> p var
R11581:11581 LamSF_Substitution <> n var
R11579:11579 LamSF_Substitution <> U var
R11596:11605 LamSF_Substitution <> lift_rec_r def
R11611:11611 LamSF_Substitution <> p var
R11609:11609 LamSF_Substitution <> n var
R11607:11607 LamSF_Substitution <> U var
R11546:11549 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11545:11545 LamSF_Substitution <> n var
R11550:11550 LamSF_Substitution <> q var
R11531:11534 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R11530:11530 LamSF_Substitution <> q var
R11536:11538 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11535:11535 LamSF_Substitution <> p var
R11539:11539 LamSF_Substitution <> n var
R11698:11707 LamSF_Substitution <> insert_Var def
R11710:11717 LamSF_Terms <> relocate def
R11749:11752 Test <> test def
R11749:11752 Test <> test def
R11799:11805 Test <> compare def
R11810:11810 Coq.Init.Datatypes <> S constr
R11814:11816 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11799:11805 Test <> compare def
R11810:11810 Coq.Init.Datatypes <> S constr
R11814:11816 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11972:11978 Test <> compare def
R11972:11978 Test <> compare def
prf 12266:12279 <> subst_rec_lift
R12298:12304 LamSF_Redexes <> redexes ind
R12314:12316 Coq.Init.Datatypes <> nat ind
R12327:12330 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12363:12365 Coq.Init.Logic <> :type_scope:x_'='_x not
R12331:12341 LamSF_Substitution <> subst_rec_r def
R12362:12362 LamSF_Substitution <> q var
R12360:12360 LamSF_Substitution <> V var
R12344:12349 LamSF_Substitution <> lift_r def
R12357:12357 LamSF_Substitution <> U var
R12352:12352 Coq.Init.Datatypes <> S constr
R12354:12354 LamSF_Substitution <> p var
R12366:12371 LamSF_Substitution <> lift_r def
R12375:12375 LamSF_Substitution <> U var
R12373:12373 LamSF_Substitution <> p var
R12322:12325 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R12321:12321 LamSF_Substitution <> q var
R12326:12326 LamSF_Substitution <> p var
R12392:12397 LamSF_Substitution <> lift_r def
R12424:12441 LamSF_Substitution <> subst_rec_lift_rec thm
R12424:12441 LamSF_Substitution <> subst_rec_lift_rec thm
R12424:12441 LamSF_Substitution <> subst_rec_lift_rec thm
R12424:12441 LamSF_Substitution <> subst_rec_lift_rec thm
R12424:12441 LamSF_Substitution <> subst_rec_lift_rec thm
R12469:12476 Coq.Init.Peano <> plus_n_O thm
R12469:12476 Coq.Init.Peano <> plus_n_O thm
prf 12538:12556 <> subst_rec_subst_rec
R12577:12583 LamSF_Redexes <> redexes ind
R12593:12595 Coq.Init.Datatypes <> nat ind
R12641:12644 Coq.Init.Logic <> :type_scope:x_'='_x not
R12600:12610 LamSF_Substitution <> subst_rec_r def
R12636:12638 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12635:12635 LamSF_Substitution <> p var
R12639:12639 LamSF_Substitution <> n var
R12632:12632 LamSF_Substitution <> W var
R12613:12623 LamSF_Substitution <> subst_rec_r def
R12629:12629 LamSF_Substitution <> p var
R12627:12627 LamSF_Substitution <> U var
R12625:12625 LamSF_Substitution <> V var
R12645:12655 LamSF_Substitution <> subst_rec_r def
R12707:12707 LamSF_Substitution <> p var
R12688:12698 LamSF_Substitution <> subst_rec_r def
R12704:12704 LamSF_Substitution <> n var
R12702:12702 LamSF_Substitution <> W var
R12700:12700 LamSF_Substitution <> U var
R12658:12668 LamSF_Substitution <> subst_rec_r def
R12675:12675 Coq.Init.Datatypes <> S constr
R12679:12681 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12678:12678 LamSF_Substitution <> p var
R12682:12682 LamSF_Substitution <> n var
R12672:12672 LamSF_Substitution <> W var
R12670:12670 LamSF_Substitution <> V var
R12760:12760 Coq.Init.Datatypes <> S constr
R12763:12763 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12777:12777 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12774:12774 Coq.Init.Datatypes <> S constr
R12760:12760 Coq.Init.Datatypes <> S constr
R12763:12763 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12777:12777 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12774:12774 Coq.Init.Datatypes <> S constr
R12821:12830 LamSF_Substitution <> insert_Var def
R12847:12853 Test <> compare def
R12847:12853 Test <> compare def
R12952:12958 Test <> compare def
R12961:12961 Coq.Init.Datatypes <> S constr
R12965:12967 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12952:12958 Test <> compare def
R12961:12961 Coq.Init.Datatypes <> S constr
R12965:12967 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13105:13114 LamSF_Substitution <> insert_Var def
R13124:13130 Test <> compare def
R13140:13143 Coq.Init.Peano <> pred syndef
R13134:13134 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13124:13130 Test <> compare def
R13140:13143 Coq.Init.Peano <> pred syndef
R13134:13134 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13199:13205 Test <> compare def
R13210:13213 Coq.Init.Peano <> pred syndef
R13199:13205 Test <> compare def
R13210:13213 Coq.Init.Peano <> pred syndef
R13281:13287 Test <> compare def
R13292:13295 Coq.Init.Peano <> pred syndef
R13281:13287 Test <> compare def
R13292:13295 Coq.Init.Peano <> pred syndef
R13342:13351 LamSF_Substitution <> insert_Var def
R13361:13367 Test <> compare def
R13377:13380 Coq.Init.Peano <> pred syndef
R13371:13371 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13361:13367 Test <> compare def
R13377:13380 Coq.Init.Peano <> pred syndef
R13371:13371 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13439:13452 LamSF_Substitution <> subst_rec_lift thm
R13439:13452 LamSF_Substitution <> subst_rec_lift thm
R13439:13452 LamSF_Substitution <> subst_rec_lift thm
R13439:13452 LamSF_Substitution <> subst_rec_lift thm
R13494:13503 LamSF_Substitution <> insert_Var def
R13513:13519 Test <> compare def
R13529:13532 Coq.Init.Peano <> pred syndef
R13523:13523 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13513:13519 Test <> compare def
R13529:13532 Coq.Init.Peano <> pred syndef
R13523:13523 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13588:13594 Test <> compare def
R13588:13594 Test <> compare def
R13663:13669 Test <> compare def
R13672:13672 Coq.Init.Datatypes <> S constr
R13675:13675 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13663:13669 Test <> compare def
R13672:13672 Coq.Init.Datatypes <> S constr
R13675:13675 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13746:13755 LamSF_Substitution <> insert_Var def
R13765:13771 Test <> compare def
R13765:13771 Test <> compare def
R13831:13845 LamSF_Substitution <> subst_rec_lift1 thm
R13831:13845 LamSF_Substitution <> subst_rec_lift1 thm
R13831:13845 LamSF_Substitution <> subst_rec_lift1 thm
R13869:13875 Test <> compare def
R13878:13878 Coq.Init.Datatypes <> S constr
R13882:13884 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13869:13875 Test <> compare def
R13878:13878 Coq.Init.Datatypes <> S constr
R13882:13884 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13956:13965 LamSF_Substitution <> insert_Var def
R13975:13981 Test <> compare def
R13985:13985 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R13975:13981 Test <> compare def
R13985:13985 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14054:14060 Test <> compare def
R14054:14060 Test <> compare def
prf 14136:14152 <> subst_rec_subst_0
R14173:14179 LamSF_Redexes <> redexes ind
R14187:14189 Coq.Init.Datatypes <> nat ind
R14229:14232 Coq.Init.Logic <> :type_scope:x_'='_x not
R14194:14204 LamSF_Substitution <> subst_rec_r def
R14228:14228 LamSF_Substitution <> n var
R14226:14226 LamSF_Substitution <> W var
R14207:14217 LamSF_Substitution <> subst_rec_r def
R14221:14221 LamSF_Substitution <> U var
R14219:14219 LamSF_Substitution <> V var
R14233:14243 LamSF_Substitution <> subst_rec_r def
R14270:14280 LamSF_Substitution <> subst_rec_r def
R14286:14286 LamSF_Substitution <> n var
R14284:14284 LamSF_Substitution <> W var
R14282:14282 LamSF_Substitution <> U var
R14246:14256 LamSF_Substitution <> subst_rec_r def
R14263:14263 Coq.Init.Datatypes <> S constr
R14265:14265 LamSF_Substitution <> n var
R14260:14260 LamSF_Substitution <> W var
R14258:14258 LamSF_Substitution <> V var
R14350:14352 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14350:14352 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14366:14384 LamSF_Substitution <> subst_rec_subst_rec thm
R14366:14384 LamSF_Substitution <> subst_rec_subst_rec thm
R14366:14384 LamSF_Substitution <> subst_rec_subst_rec thm
prf 14553:14564 <> substitution
R14585:14591 LamSF_Redexes <> redexes ind
R14599:14601 Coq.Init.Datatypes <> nat ind
R14635:14638 Coq.Init.Logic <> :type_scope:x_'='_x not
R14606:14616 LamSF_Substitution <> subst_rec_r def
R14634:14634 LamSF_Substitution <> n var
R14632:14632 LamSF_Substitution <> W var
R14619:14625 LamSF_Substitution <> subst_r def
R14629:14629 LamSF_Substitution <> V var
R14627:14627 LamSF_Substitution <> U var
R14639:14645 LamSF_Substitution <> subst_r def
R14668:14678 LamSF_Substitution <> subst_rec_r def
R14685:14685 Coq.Init.Datatypes <> S constr
R14687:14687 LamSF_Substitution <> n var
R14682:14682 LamSF_Substitution <> W var
R14680:14680 LamSF_Substitution <> V var
R14648:14658 LamSF_Substitution <> subst_rec_r def
R14664:14664 LamSF_Substitution <> n var
R14662:14662 LamSF_Substitution <> W var
R14660:14660 LamSF_Substitution <> U var
R14706:14712 LamSF_Substitution <> subst_r def
R14737:14753 LamSF_Substitution <> subst_rec_subst_0 thm
R14737:14753 LamSF_Substitution <> subst_rec_subst_0 thm
prf 14832:14853 <> lift_rec_preserve_comp
R14873:14879 LamSF_Redexes <> redexes ind
R14893:14896 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14910:14912 Coq.Init.Datatypes <> nat ind
R14915:14918 LamSF_Redexes <> comp ind
R14941:14950 LamSF_Substitution <> lift_rec_r def
R14957:14957 LamSF_Substitution <> n var
R14955:14955 LamSF_Substitution <> m var
R14952:14953 LamSF_Substitution <> V1 var
R14921:14930 LamSF_Substitution <> lift_rec_r def
R14937:14937 LamSF_Substitution <> n var
R14935:14935 LamSF_Substitution <> m var
R14932:14933 LamSF_Substitution <> U1 var
R14883:14886 LamSF_Redexes <> comp ind
R14891:14892 LamSF_Substitution <> V1 var
R14888:14889 LamSF_Substitution <> U1 var
prf 15043:15065 <> subst_rec_preserve_comp
R15085:15091 LamSF_Redexes <> redexes ind
R15104:15108 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15134:15138 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15150:15152 Coq.Init.Datatypes <> nat ind
R15155:15158 LamSF_Redexes <> comp ind
R15183:15193 LamSF_Substitution <> subst_rec_r def
R15201:15201 LamSF_Substitution <> n var
R15198:15199 LamSF_Substitution <> V2 var
R15195:15196 LamSF_Substitution <> V1 var
R15161:15171 LamSF_Substitution <> subst_rec_r def
R15179:15179 LamSF_Substitution <> n var
R15176:15177 LamSF_Substitution <> U2 var
R15173:15174 LamSF_Substitution <> U1 var
R15124:15127 LamSF_Redexes <> comp ind
R15132:15133 LamSF_Substitution <> V2 var
R15129:15130 LamSF_Substitution <> U2 var
R15094:15097 LamSF_Redexes <> comp ind
R15102:15103 LamSF_Substitution <> V1 var
R15099:15100 LamSF_Substitution <> U1 var
R15282:15291 LamSF_Substitution <> insert_Var def
R15301:15307 Test <> compare def
R15301:15307 Test <> compare def
R15354:15359 LamSF_Substitution <> lift_r def
R15371:15392 LamSF_Substitution <> lift_rec_preserve_comp thm
prf 15407:15425 <> subst_preserve_comp
R15451:15457 LamSF_Redexes <> redexes ind
R15471:15474 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15485:15488 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15489:15492 LamSF_Redexes <> comp ind
R15511:15517 LamSF_Substitution <> subst_r def
R15522:15523 LamSF_Substitution <> V1 var
R15519:15520 LamSF_Substitution <> V2 var
R15495:15501 LamSF_Substitution <> subst_r def
R15506:15507 LamSF_Substitution <> U1 var
R15503:15504 LamSF_Substitution <> U2 var
R15475:15478 LamSF_Redexes <> comp ind
R15483:15484 LamSF_Substitution <> V2 var
R15480:15481 LamSF_Substitution <> U2 var
R15461:15464 LamSF_Redexes <> comp ind
R15469:15470 LamSF_Substitution <> V1 var
R15466:15467 LamSF_Substitution <> U1 var
R15549:15555 LamSF_Substitution <> subst_r def
R15572:15594 LamSF_Substitution <> subst_rec_preserve_comp thm
R15572:15594 LamSF_Substitution <> subst_rec_preserve_comp thm
prf 15671:15695 <> lift_rec_preserve_regular
R15711:15717 LamSF_Redexes <> redexes ind
R15730:15733 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15747:15749 Coq.Init.Datatypes <> nat ind
R15752:15758 LamSF_Redexes <> regular def
R15761:15770 LamSF_Substitution <> lift_rec_r def
R15776:15776 LamSF_Substitution <> n var
R15774:15774 LamSF_Substitution <> m var
R15772:15772 LamSF_Substitution <> U var
R15721:15727 LamSF_Redexes <> regular def
R15729:15729 LamSF_Substitution <> U var
prf 15900:15925 <> subst_rec_preserve_regular
R15943:15949 LamSF_Redexes <> redexes ind
R15962:15965 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15975:15978 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15990:15992 Coq.Init.Datatypes <> nat ind
R15995:16001 LamSF_Redexes <> regular def
R16004:16014 LamSF_Substitution <> subst_rec_r def
R16020:16020 LamSF_Substitution <> n var
R16018:16018 LamSF_Substitution <> V var
R16016:16016 LamSF_Substitution <> U var
R15966:15972 LamSF_Redexes <> regular def
R15974:15974 LamSF_Substitution <> V var
R15953:15959 LamSF_Redexes <> regular def
R15961:15961 LamSF_Substitution <> U var
R16098:16107 LamSF_Substitution <> insert_Var def
R16124:16130 Test <> compare def
R16124:16130 Test <> compare def
R16178:16183 LamSF_Substitution <> lift_r def
R16200:16224 LamSF_Substitution <> lift_rec_preserve_regular thm
R16200:16224 LamSF_Substitution <> lift_rec_preserve_regular thm
prf 16295:16316 <> subst_preserve_regular
R16334:16340 LamSF_Redexes <> redexes ind
R16352:16355 Coq.Init.Logic <> :type_scope:x_'->'_x not
R16365:16368 Coq.Init.Logic <> :type_scope:x_'->'_x not
R16369:16375 LamSF_Redexes <> regular def
R16378:16384 LamSF_Substitution <> subst_r def
R16388:16388 LamSF_Substitution <> V var
R16386:16386 LamSF_Substitution <> U var
R16356:16362 LamSF_Redexes <> regular def
R16364:16364 LamSF_Substitution <> V var
R16343:16349 LamSF_Redexes <> regular def
R16351:16351 LamSF_Substitution <> U var
R16406:16412 LamSF_Substitution <> subst_r def
R16437:16462 LamSF_Substitution <> subst_rec_preserve_regular thm
R16437:16462 LamSF_Substitution <> subst_rec_preserve_regular thm