-
Notifications
You must be signed in to change notification settings - Fork 3
/
LamSF_Substitution_term.glob
876 lines (876 loc) · 37.4 KB
/
LamSF_Substitution_term.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
DIGEST 8f3b23d2e8abfb6276a906ec0d770d3d
FLamSF_Substitution_term
R2065:2069 Coq.Arith.Arith <> <> lib
R2087:2090 Test <> <> lib
R2108:2114 General <> <> lib
R2132:2142 LamSF_Terms <> <> lib
R2160:2172 LamSF_Tactics <> <> lib
R2190:2194 Coq.omega.Omega <> <> lib
prf 2228:2245 <> lift_rec_null_term
R2262:2266 LamSF_Terms <> lamSF ind
R2272:2274 Coq.Init.Datatypes <> nat ind
R2292:2294 Coq.Init.Logic <> :type_scope:x_'='_x not
R2278:2285 LamSF_Terms <> lift_rec def
R2289:2289 LamSF_Substitution_term <> n var
R2287:2287 LamSF_Substitution_term <> U var
R2295:2295 LamSF_Substitution_term <> U var
prf 2370:2374 <> lift1
R2391:2395 LamSF_Terms <> lamSF ind
R2407:2409 Coq.Init.Datatypes <> nat ind
R2449:2451 Coq.Init.Logic <> :type_scope:x_'='_x not
R2414:2421 LamSF_Terms <> lift_rec def
R2448:2448 LamSF_Substitution_term <> k var
R2442:2444 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2441:2441 LamSF_Substitution_term <> j var
R2445:2445 LamSF_Substitution_term <> i var
R2424:2431 LamSF_Terms <> lift_rec def
R2437:2437 LamSF_Substitution_term <> j var
R2435:2435 LamSF_Substitution_term <> i var
R2433:2433 LamSF_Substitution_term <> U var
R2452:2459 LamSF_Terms <> lift_rec def
R2467:2469 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2466:2466 LamSF_Substitution_term <> j var
R2470:2470 LamSF_Substitution_term <> k var
R2463:2463 LamSF_Substitution_term <> i var
R2461:2461 LamSF_Substitution_term <> U var
R2536:2543 LamSF_Terms <> relocate def
R2553:2556 Test <> test def
R2570:2573 Test <> test def
R2583:2584 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2577:2577 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2553:2556 Test <> test def
R2570:2573 Test <> test def
R2583:2584 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2577:2577 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2570:2573 Test <> test def
R2583:2584 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2577:2577 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2631:2633 Coq.Init.Logic <> :type_scope:x_'='_x not
R2621:2624 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2630:2630 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2626:2628 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2639:2641 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2635:2637 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2631:2633 Coq.Init.Logic <> :type_scope:x_'='_x not
R2621:2624 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2630:2630 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2626:2628 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2639:2641 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2635:2637 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2674:2677 Test <> test def
R2681:2683 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2674:2677 Test <> test def
R2681:2683 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2722:2729 LamSF_Terms <> relocate def
R2742:2742 Coq.Init.Datatypes <> S constr
R2745:2745 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2757:2758 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2759:2759 Coq.Init.Datatypes <> S constr
R2742:2742 Coq.Init.Datatypes <> S constr
R2745:2745 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2757:2758 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2759:2759 Coq.Init.Datatypes <> S constr
prf 2806:2818 <> lift_lift_rec
R2835:2839 LamSF_Terms <> lamSF ind
R2853:2855 Coq.Init.Datatypes <> nat ind
R2866:2870 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2906:2908 Coq.Init.Logic <> :type_scope:x_'='_x not
R2871:2878 LamSF_Terms <> lift_rec def
R2905:2905 LamSF_Substitution_term <> k var
R2899:2901 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R2898:2898 LamSF_Substitution_term <> p var
R2902:2902 LamSF_Substitution_term <> n var
R2881:2888 LamSF_Terms <> lift_rec def
R2894:2894 LamSF_Substitution_term <> p var
R2892:2892 LamSF_Substitution_term <> i var
R2890:2890 LamSF_Substitution_term <> U var
R2909:2916 LamSF_Terms <> lift_rec def
R2937:2937 LamSF_Substitution_term <> p var
R2935:2935 LamSF_Substitution_term <> i var
R2919:2926 LamSF_Terms <> lift_rec def
R2932:2932 LamSF_Substitution_term <> k var
R2930:2930 LamSF_Substitution_term <> n var
R2928:2928 LamSF_Substitution_term <> U var
R2861:2864 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R2860:2860 LamSF_Substitution_term <> i var
R2865:2865 LamSF_Substitution_term <> n var
R3012:3019 LamSF_Terms <> relocate def
R3027:3030 Test <> test def
R3027:3030 Test <> test def
R3066:3069 Test <> test def
R3066:3069 Test <> test def
R3106:3109 Test <> test def
R3120:3120 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3113:3113 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3106:3109 Test <> test def
R3120:3120 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3113:3113 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3154:3157 Test <> test def
R3163:3163 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3154:3157 Test <> test def
R3163:3163 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3206:3208 Coq.Init.Logic <> :type_scope:x_'='_x not
R3200:3201 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3205:3205 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3203:3203 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3210:3212 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3216:3216 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3214:3214 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3206:3208 Coq.Init.Logic <> :type_scope:x_'='_x not
R3200:3201 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3205:3205 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3203:3203 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3210:3212 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3216:3216 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3214:3214 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3254:3257 Test <> test def
R3268:3268 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3261:3261 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3254:3257 Test <> test def
R3268:3268 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3261:3261 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3302:3305 Test <> test def
R3302:3305 Test <> test def
R3341:3344 Test <> test def
R3341:3344 Test <> test def
R3381:3384 Test <> test def
R3388:3388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3381:3384 Test <> test def
R3388:3388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3425:3428 Test <> test def
R3425:3428 Test <> test def
R3478:3478 Coq.Init.Datatypes <> S constr
R3481:3483 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3495:3497 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3498:3498 Coq.Init.Datatypes <> S constr
R3478:3478 Coq.Init.Datatypes <> S constr
R3481:3483 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3495:3497 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3498:3498 Coq.Init.Datatypes <> S constr
prf 3614:3627 <> lift_lift_term
R3644:3648 LamSF_Terms <> lamSF ind
R3660:3662 Coq.Init.Datatypes <> nat ind
R3695:3697 Coq.Init.Logic <> :type_scope:x_'='_x not
R3667:3674 LamSF_Terms <> lift_rec def
R3694:3694 LamSF_Substitution_term <> k var
R3689:3690 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R3688:3688 LamSF_Substitution_term <> p var
R3691:3691 LamSF_Substitution_term <> n var
R3677:3680 LamSF_Terms <> lift def
R3684:3684 LamSF_Substitution_term <> U var
R3682:3682 LamSF_Substitution_term <> p var
R3698:3701 LamSF_Terms <> lift def
R3706:3713 LamSF_Terms <> lift_rec def
R3719:3719 LamSF_Substitution_term <> k var
R3717:3717 LamSF_Substitution_term <> n var
R3715:3715 LamSF_Substitution_term <> U var
R3703:3703 LamSF_Substitution_term <> p var
R3737:3740 LamSF_Terms <> lift def
R3765:3777 LamSF_Substitution_term <> lift_lift_rec thm
R3765:3777 LamSF_Substitution_term <> lift_lift_rec thm
prf 3812:3819 <> liftrecO
R3835:3839 LamSF_Terms <> lamSF ind
R3847:3849 Coq.Init.Datatypes <> nat ind
R3867:3869 Coq.Init.Logic <> :type_scope:x_'='_x not
R3853:3860 LamSF_Terms <> lift_rec def
R3864:3864 LamSF_Substitution_term <> n var
R3862:3862 LamSF_Substitution_term <> U var
R3870:3870 LamSF_Substitution_term <> U var
prf 3972:3976 <> liftO
R3992:3996 LamSF_Terms <> lamSF ind
R4009:4011 Coq.Init.Logic <> :type_scope:x_'='_x not
R4001:4004 LamSF_Terms <> lift def
R4008:4008 LamSF_Substitution_term <> U var
R4012:4012 LamSF_Substitution_term <> U var
R4029:4032 LamSF_Terms <> lift def
R4060:4067 LamSF_Substitution_term <> liftrecO thm
R4060:4067 LamSF_Substitution_term <> liftrecO thm
prf 4082:4098 <> lift_rec_lift_rec
R4115:4119 LamSF_Terms <> lamSF ind
R4133:4135 Coq.Init.Datatypes <> nat ind
R4150:4154 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4161:4164 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4194:4196 Coq.Init.Logic <> :type_scope:x_'='_x not
R4165:4172 LamSF_Terms <> lift_rec def
R4193:4193 LamSF_Substitution_term <> p var
R4191:4191 LamSF_Substitution_term <> k var
R4175:4182 LamSF_Terms <> lift_rec def
R4188:4188 LamSF_Substitution_term <> n var
R4186:4186 LamSF_Substitution_term <> i var
R4184:4184 LamSF_Substitution_term <> U var
R4197:4204 LamSF_Terms <> lift_rec def
R4212:4214 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4211:4211 LamSF_Substitution_term <> p var
R4215:4215 LamSF_Substitution_term <> n var
R4208:4208 LamSF_Substitution_term <> i var
R4206:4206 LamSF_Substitution_term <> U var
R4156:4159 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4155:4155 LamSF_Substitution_term <> i var
R4160:4160 LamSF_Substitution_term <> k var
R4141:4144 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4140:4140 LamSF_Substitution_term <> k var
R4146:4148 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4145:4145 LamSF_Substitution_term <> i var
R4149:4149 LamSF_Substitution_term <> n var
R4276:4283 LamSF_Terms <> relocate def
R4292:4295 Test <> test def
R4292:4295 Test <> test def
R4331:4334 Test <> test def
R4341:4343 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4331:4334 Test <> test def
R4341:4343 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4382:4383 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4388:4388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4386:4386 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4403:4405 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4398:4400 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4382:4383 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4388:4388 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4386:4386 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4403:4405 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4398:4400 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4431:4434 Test <> test def
R4431:4434 Test <> test def
prf 4588:4600 <> lift_rec_lift
R4617:4621 LamSF_Terms <> lamSF ind
R4636:4638 Coq.Init.Datatypes <> nat ind
R4649:4652 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4678:4680 Coq.Init.Logic <> :type_scope:x_'='_x not
R4653:4660 LamSF_Terms <> lift_rec def
R4677:4677 LamSF_Substitution_term <> p var
R4675:4675 LamSF_Substitution_term <> k var
R4663:4666 LamSF_Terms <> lift def
R4671:4671 LamSF_Substitution_term <> U var
R4669:4669 LamSF_Substitution_term <> n var
R4681:4684 LamSF_Terms <> lift def
R4694:4694 LamSF_Substitution_term <> U var
R4688:4690 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4687:4687 LamSF_Substitution_term <> p var
R4691:4691 LamSF_Substitution_term <> n var
R4644:4647 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4643:4643 LamSF_Substitution_term <> k var
R4648:4648 LamSF_Substitution_term <> n var
R4711:4714 LamSF_Terms <> lift def
R4741:4757 LamSF_Substitution_term <> lift_rec_lift_rec thm
R4741:4757 LamSF_Substitution_term <> lift_rec_lift_rec thm
R4741:4757 LamSF_Substitution_term <> lift_rec_lift_rec thm
R4741:4757 LamSF_Substitution_term <> lift_rec_lift_rec thm
R4741:4757 LamSF_Substitution_term <> lift_rec_lift_rec thm
prf 4794:4800 <> gt_plus
R4819:4821 Coq.Init.Datatypes <> nat ind
R4829:4832 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4834:4835 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4833:4833 LamSF_Substitution_term <> i var
R4836:4836 LamSF_Substitution_term <> n var
R4825:4825 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R4824:4824 LamSF_Substitution_term <> i var
R4827:4827 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4826:4826 LamSF_Substitution_term <> m var
R4828:4828 LamSF_Substitution_term <> n var
prf 4923:4929 <> le_plus
R4948:4950 Coq.Init.Datatypes <> nat ind
R4962:4965 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4967:4969 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4966:4966 LamSF_Substitution_term <> i var
R4970:4970 LamSF_Substitution_term <> n var
R4957:4960 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R4954:4955 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4953:4953 LamSF_Substitution_term <> i var
R4956:4956 LamSF_Substitution_term <> m var
R4961:4961 LamSF_Substitution_term <> n var
R5064:5064 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5065:5065 Coq.Init.Datatypes <> S constr
R5048:5055 Coq.Arith.Le <> le_trans syndef
R5064:5064 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5065:5065 Coq.Init.Datatypes <> S constr
R5048:5055 Coq.Arith.Le <> le_trans syndef
R5145:5146 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5141:5141 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5142:5142 Coq.Init.Datatypes <> S constr
R5147:5147 Coq.Init.Datatypes <> S constr
R5161:5169 Coq.Arith.Gt <> le_not_gt thm
R5182:5183 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R5184:5184 Coq.Init.Datatypes <> S constr
R5195:5195 Coq.Init.Datatypes <> S constr
R5199:5199 Coq.Init.Peano <> :nat_scope:x_'+'_x not
prf 5297:5304 <> subst_eq
R5323:5327 LamSF_Terms <> lamSF ind
R5335:5337 Coq.Init.Datatypes <> nat ind
R5362:5364 Coq.Init.Logic <> :type_scope:x_'='_x not
R5341:5349 LamSF_Terms <> subst_rec def
R5361:5361 LamSF_Substitution_term <> n var
R5359:5359 LamSF_Substitution_term <> U var
R5352:5354 LamSF_Terms <> Ref constr
R5356:5356 LamSF_Substitution_term <> n var
R5365:5368 LamSF_Terms <> lift def
R5372:5372 LamSF_Substitution_term <> U var
R5370:5370 LamSF_Substitution_term <> n var
R5405:5414 LamSF_Terms <> insert_Ref def
R5443:5449 Test <> compare def
R5443:5449 Test <> compare def
prf 5553:5560 <> subst_gt
R5579:5583 LamSF_Terms <> lamSF ind
R5593:5595 Coq.Init.Datatypes <> nat ind
R5605:5608 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5630:5632 Coq.Init.Logic <> :type_scope:x_'='_x not
R5609:5617 LamSF_Terms <> subst_rec def
R5629:5629 LamSF_Substitution_term <> p var
R5627:5627 LamSF_Substitution_term <> U var
R5620:5622 LamSF_Terms <> Ref constr
R5624:5624 LamSF_Substitution_term <> n var
R5633:5635 LamSF_Terms <> Ref constr
R5638:5641 Coq.Init.Peano <> pred syndef
R5643:5643 LamSF_Substitution_term <> n var
R5601:5603 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5600:5600 LamSF_Substitution_term <> n var
R5604:5604 LamSF_Substitution_term <> p var
R5676:5685 LamSF_Terms <> insert_Ref def
R5710:5716 Test <> compare def
R5710:5716 Test <> compare def
R5779:5781 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5779:5781 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5846:5848 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5846:5848 Coq.Init.Peano <> :nat_scope:x_'>'_x not
prf 5883:5890 <> subst_lt
R5909:5913 LamSF_Terms <> lamSF ind
R5923:5925 Coq.Init.Datatypes <> nat ind
R5934:5937 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5959:5961 Coq.Init.Logic <> :type_scope:x_'='_x not
R5938:5946 LamSF_Terms <> subst_rec def
R5958:5958 LamSF_Substitution_term <> p var
R5956:5956 LamSF_Substitution_term <> U var
R5949:5951 LamSF_Terms <> Ref constr
R5953:5953 LamSF_Substitution_term <> n var
R5962:5964 LamSF_Terms <> Ref constr
R5966:5966 LamSF_Substitution_term <> n var
R5930:5932 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R5929:5929 LamSF_Substitution_term <> p var
R5933:5933 LamSF_Substitution_term <> n var
R5998:6007 LamSF_Terms <> insert_Ref def
R6032:6038 Test <> compare def
R6032:6038 Test <> compare def
R6084:6086 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R6084:6086 Coq.Init.Peano <> :nat_scope:x_'>'_x not
prf 6214:6231 <> lift_rec_subst_rec
R6250:6254 LamSF_Terms <> lamSF ind
R6266:6268 Coq.Init.Datatypes <> nat ind
R6309:6312 Coq.Init.Logic <> :type_scope:x_'='_x not
R6273:6280 LamSF_Terms <> lift_rec def
R6308:6308 LamSF_Substitution_term <> k var
R6302:6304 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6301:6301 LamSF_Substitution_term <> p var
R6305:6305 LamSF_Substitution_term <> n var
R6283:6291 LamSF_Terms <> subst_rec def
R6297:6297 LamSF_Substitution_term <> p var
R6295:6295 LamSF_Substitution_term <> U var
R6293:6293 LamSF_Substitution_term <> V var
R6313:6321 LamSF_Terms <> subst_rec def
R6367:6367 LamSF_Substitution_term <> p var
R6351:6358 LamSF_Terms <> lift_rec def
R6364:6364 LamSF_Substitution_term <> k var
R6362:6362 LamSF_Substitution_term <> n var
R6360:6360 LamSF_Substitution_term <> U var
R6324:6331 LamSF_Terms <> lift_rec def
R6347:6347 LamSF_Substitution_term <> k var
R6336:6336 Coq.Init.Datatypes <> S constr
R6340:6342 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6339:6339 LamSF_Substitution_term <> p var
R6343:6343 LamSF_Substitution_term <> n var
R6333:6333 LamSF_Substitution_term <> V var
R6428:6437 LamSF_Terms <> insert_Ref def
R6440:6447 LamSF_Terms <> relocate def
R6464:6467 Test <> test def
R6470:6470 Coq.Init.Datatypes <> S constr
R6473:6475 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6491:6497 Test <> compare def
R6464:6467 Test <> test def
R6470:6470 Coq.Init.Datatypes <> S constr
R6473:6475 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6491:6497 Test <> compare def
R6491:6497 Test <> compare def
R6529:6535 Test <> compare def
R6541:6541 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6529:6535 Test <> compare def
R6541:6541 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6529:6535 Test <> compare def
R6541:6541 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6566:6573 LamSF_Terms <> relocate def
R6582:6585 Test <> test def
R6595:6598 Coq.Init.Peano <> pred syndef
R6589:6589 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6582:6585 Test <> test def
R6595:6598 Coq.Init.Peano <> pred syndef
R6589:6589 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6647:6649 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6650:6653 Coq.Init.Peano <> pred syndef
R6664:6667 Coq.Init.Peano <> pred syndef
R6671:6673 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6647:6649 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6650:6653 Coq.Init.Peano <> pred syndef
R6664:6667 Coq.Init.Peano <> pred syndef
R6671:6673 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6752:6759 LamSF_Terms <> relocate def
R6767:6770 Test <> test def
R6779:6782 Coq.Init.Peano <> pred syndef
R6773:6773 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6767:6770 Test <> test def
R6779:6782 Coq.Init.Peano <> pred syndef
R6773:6773 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6815:6818 LamSF_Terms <> lift def
R6829:6841 LamSF_Substitution_term <> lift_lift_rec thm
R6829:6841 LamSF_Substitution_term <> lift_lift_rec thm
R6829:6841 LamSF_Substitution_term <> lift_lift_rec thm
R6829:6841 LamSF_Substitution_term <> lift_lift_rec thm
R6865:6872 LamSF_Terms <> relocate def
R6881:6884 Test <> test def
R6888:6888 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6881:6884 Test <> test def
R6888:6888 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6925:6925 Coq.Init.Datatypes <> S constr
R6928:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6942:6944 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6939:6939 Coq.Init.Datatypes <> S constr
R6925:6925 Coq.Init.Datatypes <> S constr
R6928:6928 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6942:6944 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6939:6939 Coq.Init.Datatypes <> S constr
prf 6986:6995 <> lift_subst
R7014:7018 LamSF_Terms <> lamSF ind
R7028:7030 Coq.Init.Datatypes <> nat ind
R7059:7062 Coq.Init.Logic <> :type_scope:x_'='_x not
R7035:7042 LamSF_Terms <> lift_rec def
R7058:7058 LamSF_Substitution_term <> k var
R7056:7056 LamSF_Substitution_term <> n var
R7045:7049 LamSF_Terms <> subst def
R7053:7053 LamSF_Substitution_term <> V var
R7051:7051 LamSF_Substitution_term <> U var
R7063:7067 LamSF_Terms <> subst def
R7087:7094 LamSF_Terms <> lift_rec def
R7104:7104 LamSF_Substitution_term <> k var
R7099:7099 Coq.Init.Datatypes <> S constr
R7101:7101 LamSF_Substitution_term <> n var
R7096:7096 LamSF_Substitution_term <> V var
R7070:7077 LamSF_Terms <> lift_rec def
R7083:7083 LamSF_Substitution_term <> k var
R7081:7081 LamSF_Substitution_term <> n var
R7079:7079 LamSF_Substitution_term <> U var
R7122:7126 LamSF_Terms <> subst def
R7154:7154 Coq.Init.Datatypes <> S constr
R7165:7165 Coq.Init.Datatypes <> S constr
R7169:7171 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7154:7154 Coq.Init.Datatypes <> S constr
R7165:7165 Coq.Init.Datatypes <> S constr
R7169:7171 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7182:7199 LamSF_Substitution_term <> lift_rec_subst_rec thm
R7182:7199 LamSF_Substitution_term <> lift_rec_subst_rec thm
prf 7269:7287 <> subst_rec_lift_rec1
R7306:7310 LamSF_Terms <> lamSF ind
R7322:7324 Coq.Init.Datatypes <> nat ind
R7335:7339 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7376:7379 Coq.Init.Logic <> :type_scope:x_'='_x not
R7340:7348 LamSF_Terms <> subst_rec def
R7371:7373 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7370:7370 LamSF_Substitution_term <> p var
R7374:7374 LamSF_Substitution_term <> n var
R7367:7367 LamSF_Substitution_term <> V var
R7351:7358 LamSF_Terms <> lift_rec def
R7364:7364 LamSF_Substitution_term <> p var
R7362:7362 LamSF_Substitution_term <> k var
R7360:7360 LamSF_Substitution_term <> U var
R7380:7387 LamSF_Terms <> lift_rec def
R7409:7409 LamSF_Substitution_term <> p var
R7407:7407 LamSF_Substitution_term <> k var
R7390:7398 LamSF_Terms <> subst_rec def
R7404:7404 LamSF_Substitution_term <> n var
R7402:7402 LamSF_Substitution_term <> V var
R7400:7400 LamSF_Substitution_term <> U var
R7330:7333 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R7329:7329 LamSF_Substitution_term <> k var
R7334:7334 LamSF_Substitution_term <> n var
R7491:7500 LamSF_Terms <> insert_Ref def
R7503:7510 LamSF_Terms <> relocate def
R7519:7522 Test <> test def
R7519:7522 Test <> test def
R7547:7553 Test <> compare def
R7547:7553 Test <> compare def
R7622:7628 Test <> compare def
R7639:7639 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7632:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7622:7628 Test <> compare def
R7639:7639 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7632:7632 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7696:7703 LamSF_Terms <> relocate def
R7712:7715 Test <> test def
R7720:7723 Coq.Init.Peano <> pred syndef
R7712:7715 Test <> test def
R7720:7723 Coq.Init.Peano <> pred syndef
R7770:7772 Coq.Init.Logic <> :type_scope:x_'='_x not
R7760:7763 Coq.Init.Peano <> pred syndef
R7767:7767 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7774:7776 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7777:7780 Coq.Init.Peano <> pred syndef
R7770:7772 Coq.Init.Logic <> :type_scope:x_'='_x not
R7760:7763 Coq.Init.Peano <> pred syndef
R7767:7767 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7774:7776 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7777:7780 Coq.Init.Peano <> pred syndef
R7815:7821 Test <> compare def
R7832:7832 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7825:7825 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7815:7821 Test <> compare def
R7832:7832 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7825:7825 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7889:7892 LamSF_Terms <> lift def
R7903:7919 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7903:7919 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7903:7919 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7903:7919 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7903:7919 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7953:7956 LamSF_Terms <> lift def
R7967:7983 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7967:7983 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7967:7983 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7967:7983 LamSF_Substitution_term <> lift_rec_lift_rec thm
R7967:7983 LamSF_Substitution_term <> lift_rec_lift_rec thm
R8015:8021 Test <> compare def
R8032:8032 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8025:8025 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8015:8021 Test <> compare def
R8032:8032 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8025:8025 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8089:8096 LamSF_Terms <> relocate def
R8105:8108 Test <> test def
R8105:8108 Test <> test def
R8144:8150 Test <> compare def
R8154:8154 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8144:8150 Test <> compare def
R8154:8154 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8222:8228 Test <> compare def
R8222:8228 Test <> compare def
R8298:8305 LamSF_Terms <> relocate def
R8314:8317 Test <> test def
R8314:8317 Test <> test def
R8376:8376 Coq.Init.Datatypes <> S constr
R8379:8381 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8393:8395 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8396:8396 Coq.Init.Datatypes <> S constr
R8376:8376 Coq.Init.Datatypes <> S constr
R8379:8381 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8393:8395 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8396:8396 Coq.Init.Datatypes <> S constr
prf 8512:8526 <> subst_rec_lift1
R8545:8549 LamSF_Terms <> lamSF ind
R8559:8561 Coq.Init.Datatypes <> nat ind
R8596:8598 Coq.Init.Logic <> :type_scope:x_'='_x not
R8566:8574 LamSF_Terms <> subst_rec def
R8591:8593 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8590:8590 LamSF_Substitution_term <> p var
R8594:8594 LamSF_Substitution_term <> n var
R8587:8587 LamSF_Substitution_term <> V var
R8577:8580 LamSF_Terms <> lift def
R8584:8584 LamSF_Substitution_term <> U var
R8582:8582 LamSF_Substitution_term <> p var
R8599:8602 LamSF_Terms <> lift def
R8607:8615 LamSF_Terms <> subst_rec def
R8621:8621 LamSF_Substitution_term <> n var
R8619:8619 LamSF_Substitution_term <> V var
R8617:8617 LamSF_Substitution_term <> U var
R8604:8604 LamSF_Substitution_term <> p var
R8639:8642 LamSF_Terms <> lift def
R8669:8687 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R8669:8687 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R8669:8687 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R8669:8687 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
prf 8724:8741 <> subst_rec_lift_rec
R8760:8764 LamSF_Terms <> lamSF ind
R8776:8778 Coq.Init.Datatypes <> nat ind
R8793:8797 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8804:8807 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8842:8844 Coq.Init.Logic <> :type_scope:x_'='_x not
R8808:8816 LamSF_Terms <> subst_rec def
R8841:8841 LamSF_Substitution_term <> q var
R8839:8839 LamSF_Substitution_term <> V var
R8819:8826 LamSF_Terms <> lift_rec def
R8833:8833 Coq.Init.Datatypes <> S constr
R8835:8835 LamSF_Substitution_term <> p var
R8830:8830 LamSF_Substitution_term <> n var
R8828:8828 LamSF_Substitution_term <> U var
R8845:8852 LamSF_Terms <> lift_rec def
R8858:8858 LamSF_Substitution_term <> p var
R8856:8856 LamSF_Substitution_term <> n var
R8854:8854 LamSF_Substitution_term <> U var
R8799:8802 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8798:8798 LamSF_Substitution_term <> n var
R8803:8803 LamSF_Substitution_term <> q var
R8784:8787 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R8783:8783 LamSF_Substitution_term <> q var
R8789:8791 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8788:8788 LamSF_Substitution_term <> p var
R8792:8792 LamSF_Substitution_term <> n var
R8930:8937 LamSF_Terms <> relocate def
R8945:8948 Test <> test def
R8945:8948 Test <> test def
R8976:8985 LamSF_Terms <> insert_Ref def
R8994:9000 Test <> compare def
R9005:9005 Coq.Init.Datatypes <> S constr
R9008:9008 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8994:9000 Test <> compare def
R9005:9005 Coq.Init.Datatypes <> S constr
R9008:9008 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9077:9086 LamSF_Terms <> insert_Ref def
R9095:9101 Test <> compare def
R9095:9101 Test <> compare def
prf 9286:9304 <> subst_rec_subst_rec
R9325:9329 LamSF_Terms <> lamSF ind
R9339:9341 Coq.Init.Datatypes <> nat ind
R9383:9386 Coq.Init.Logic <> :type_scope:x_'='_x not
R9346:9354 LamSF_Terms <> subst_rec def
R9378:9380 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9377:9377 LamSF_Substitution_term <> p var
R9381:9381 LamSF_Substitution_term <> n var
R9374:9374 LamSF_Substitution_term <> W var
R9357:9365 LamSF_Terms <> subst_rec def
R9371:9371 LamSF_Substitution_term <> p var
R9369:9369 LamSF_Substitution_term <> U var
R9367:9367 LamSF_Substitution_term <> V var
R9387:9395 LamSF_Terms <> subst_rec def
R9443:9443 LamSF_Substitution_term <> p var
R9426:9434 LamSF_Terms <> subst_rec def
R9440:9440 LamSF_Substitution_term <> n var
R9438:9438 LamSF_Substitution_term <> W var
R9436:9436 LamSF_Substitution_term <> U var
R9398:9406 LamSF_Terms <> subst_rec def
R9413:9413 Coq.Init.Datatypes <> S constr
R9417:9419 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9416:9416 LamSF_Substitution_term <> p var
R9420:9420 LamSF_Substitution_term <> n var
R9410:9410 LamSF_Substitution_term <> W var
R9408:9408 LamSF_Substitution_term <> V var
R9493:9502 LamSF_Terms <> insert_Ref def
R9519:9525 Test <> compare def
R9519:9525 Test <> compare def
R9571:9577 Test <> compare def
R9580:9580 Coq.Init.Datatypes <> S constr
R9584:9586 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9571:9577 Test <> compare def
R9580:9580 Coq.Init.Datatypes <> S constr
R9584:9586 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9647:9656 LamSF_Terms <> insert_Ref def
R9665:9671 Test <> compare def
R9681:9684 Coq.Init.Peano <> pred syndef
R9675:9675 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9665:9671 Test <> compare def
R9681:9684 Coq.Init.Peano <> pred syndef
R9675:9675 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9751:9757 Test <> compare def
R9762:9765 Coq.Init.Peano <> pred syndef
R9751:9757 Test <> compare def
R9762:9765 Coq.Init.Peano <> pred syndef
R9833:9836 LamSF_Terms <> lift def
R9858:9867 LamSF_Terms <> insert_Ref def
R9877:9883 Test <> compare def
R9893:9896 Coq.Init.Peano <> pred syndef
R9887:9887 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9877:9883 Test <> compare def
R9893:9896 Coq.Init.Peano <> pred syndef
R9887:9887 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9971:9974 LamSF_Terms <> lift def
R9986:10003 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9986:10003 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9986:10003 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9986:10003 LamSF_Substitution_term <> subst_rec_lift_rec thm
R9986:10003 LamSF_Substitution_term <> subst_rec_lift_rec thm
R10036:10045 LamSF_Terms <> insert_Ref def
R10054:10060 Test <> compare def
R10070:10073 Coq.Init.Peano <> pred syndef
R10064:10064 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10054:10060 Test <> compare def
R10070:10073 Coq.Init.Peano <> pred syndef
R10064:10064 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10140:10146 Test <> compare def
R10140:10146 Test <> compare def
R10215:10221 Test <> compare def
R10224:10224 Coq.Init.Datatypes <> S constr
R10228:10230 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10215:10221 Test <> compare def
R10224:10224 Coq.Init.Datatypes <> S constr
R10228:10230 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10301:10310 LamSF_Terms <> insert_Ref def
R10319:10325 Test <> compare def
R10319:10325 Test <> compare def
R10395:10398 LamSF_Terms <> lift def
R10418:10436 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R10418:10436 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R10418:10436 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R10418:10436 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R10467:10476 LamSF_Terms <> insert_Ref def
R10485:10491 Test <> compare def
R10495:10495 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10485:10491 Test <> compare def
R10495:10495 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10562:10568 Test <> compare def
R10571:10571 Coq.Init.Datatypes <> S constr
R10574:10574 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10562:10568 Test <> compare def
R10571:10571 Coq.Init.Datatypes <> S constr
R10574:10574 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10645:10654 LamSF_Terms <> insert_Ref def
R10663:10669 Test <> compare def
R10663:10669 Test <> compare def
R10740:10740 Coq.Init.Datatypes <> S constr
R10743:10745 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10759:10761 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10756:10756 Coq.Init.Datatypes <> S constr
R10740:10740 Coq.Init.Datatypes <> S constr
R10743:10745 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10759:10761 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R10756:10756 Coq.Init.Datatypes <> S constr
prf 10819:10835 <> subst_rec_subst_0
R10856:10860 LamSF_Terms <> lamSF ind
R10868:10870 Coq.Init.Datatypes <> nat ind
R10906:10909 Coq.Init.Logic <> :type_scope:x_'='_x not
R10875:10883 LamSF_Terms <> subst_rec def
R10905:10905 LamSF_Substitution_term <> n var
R10903:10903 LamSF_Substitution_term <> W var
R10886:10894 LamSF_Terms <> subst_rec def
R10898:10898 LamSF_Substitution_term <> U var
R10896:10896 LamSF_Substitution_term <> V var
R10910:10918 LamSF_Terms <> subst_rec def
R10943:10951 LamSF_Terms <> subst_rec def
R10957:10957 LamSF_Substitution_term <> n var
R10955:10955 LamSF_Substitution_term <> W var
R10953:10953 LamSF_Substitution_term <> U var
R10921:10929 LamSF_Terms <> subst_rec def
R10936:10936 Coq.Init.Datatypes <> S constr
R10938:10938 LamSF_Substitution_term <> n var
R10933:10933 LamSF_Substitution_term <> W var
R10931:10931 LamSF_Substitution_term <> V var
R11021:11023 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11021:11023 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11059:11077 LamSF_Substitution_term <> subst_rec_subst_rec thm
R11059:11077 LamSF_Substitution_term <> subst_rec_subst_rec thm
R11059:11077 LamSF_Substitution_term <> subst_rec_subst_rec thm
prf 11211:11222 <> substitution
R11243:11247 LamSF_Terms <> lamSF ind
R11255:11257 Coq.Init.Datatypes <> nat ind
R11287:11290 Coq.Init.Logic <> :type_scope:x_'='_x not
R11262:11270 LamSF_Terms <> subst_rec def
R11286:11286 LamSF_Substitution_term <> n var
R11284:11284 LamSF_Substitution_term <> W var
R11273:11277 LamSF_Terms <> subst def
R11281:11281 LamSF_Substitution_term <> V var
R11279:11279 LamSF_Substitution_term <> U var
R11291:11295 LamSF_Terms <> subst def
R11316:11324 LamSF_Terms <> subst_rec def
R11331:11331 Coq.Init.Datatypes <> S constr
R11333:11333 LamSF_Substitution_term <> n var
R11328:11328 LamSF_Substitution_term <> W var
R11326:11326 LamSF_Substitution_term <> V var
R11298:11306 LamSF_Terms <> subst_rec def
R11312:11312 LamSF_Substitution_term <> n var
R11310:11310 LamSF_Substitution_term <> W var
R11308:11308 LamSF_Substitution_term <> U var
R11352:11356 LamSF_Terms <> subst def
R11381:11397 LamSF_Substitution_term <> subst_rec_subst_0 thm
R11381:11397 LamSF_Substitution_term <> subst_rec_subst_0 thm
prf 11462:11474 <> lift_rec_null
R11491:11495 LamSF_Terms <> lamSF ind
R11502:11504 Coq.Init.Datatypes <> nat ind
R11522:11524 Coq.Init.Logic <> :type_scope:x_'='_x not
R11508:11515 LamSF_Terms <> lift_rec def
R11519:11519 LamSF_Substitution_term <> n var
R11517:11517 LamSF_Substitution_term <> U var
R11525:11525 LamSF_Substitution_term <> U var
R11575:11587 LamSF_Tactics <> relocate_null thm
R11575:11587 LamSF_Tactics <> relocate_null thm
R11575:11587 LamSF_Tactics <> relocate_null thm
prf 11614:11628 <> subst_lift_null
R11646:11650 LamSF_Terms <> lamSF ind
R11657:11659 Coq.Init.Datatypes <> nat ind
R11693:11695 Coq.Init.Logic <> :type_scope:x_'='_x not
R11663:11671 LamSF_Terms <> subst_rec def
R11692:11692 LamSF_Substitution_term <> n var
R11690:11690 LamSF_Substitution_term <> V var
R11674:11681 LamSF_Terms <> lift_rec def
R11685:11685 LamSF_Substitution_term <> n var
R11683:11683 LamSF_Substitution_term <> W var
R11696:11696 LamSF_Substitution_term <> W var
R11745:11754 LamSF_Terms <> insert_Ref def
R11765:11772 LamSF_Terms <> relocate def
R11781:11784 Test <> test def
R11781:11784 Test <> test def
R11810:11816 Test <> compare def
R11822:11822 Coq.Init.Datatypes <> S constr
R11810:11816 Test <> compare def
R11822:11822 Coq.Init.Datatypes <> S constr
R11881:11887 Test <> compare def
R11881:11887 Test <> compare def
prf 11980:11993 <> lift_rec_lift2
R12039:12041 Coq.Init.Logic <> :type_scope:x_'='_x not
R12012:12019 LamSF_Terms <> lift_rec def
R12038:12038 LamSF_Substitution_term <> k var
R12033:12033 Coq.Init.Datatypes <> S constr
R12035:12035 LamSF_Substitution_term <> n var
R12022:12025 LamSF_Terms <> lift def
R12029:12029 LamSF_Substitution_term <> M var
R12042:12045 LamSF_Terms <> lift def
R12050:12057 LamSF_Terms <> lift_rec def
R12063:12063 LamSF_Substitution_term <> k var
R12061:12061 LamSF_Substitution_term <> n var
R12059:12059 LamSF_Substitution_term <> M var
R12092:12095 LamSF_Terms <> lift def
R12108:12108 Coq.Init.Datatypes <> S constr
R12120:12120 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12108:12108 Coq.Init.Datatypes <> S constr
R12120:12120 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12142:12154 LamSF_Substitution_term <> lift_lift_rec thm
R12142:12154 LamSF_Substitution_term <> lift_lift_rec thm
R12142:12154 LamSF_Substitution_term <> lift_lift_rec thm
R12142:12154 LamSF_Substitution_term <> lift_lift_rec thm
prf 12183:12196 <> relocate_null2
R12230:12232 Coq.Init.Logic <> :type_scope:x_'='_x not
R12212:12219 LamSF_Terms <> relocate def
R12229:12229 LamSF_Substitution_term <> k var
R12224:12224 Coq.Init.Datatypes <> S constr
R12226:12226 LamSF_Substitution_term <> n var
prf 12267:12281 <> subst_rec_lift2
R12329:12332 Coq.Init.Logic <> :type_scope:x_'='_x not
R12301:12309 LamSF_Terms <> subst_rec def
R12325:12325 Coq.Init.Datatypes <> S constr
R12327:12327 LamSF_Substitution_term <> n var
R12322:12322 LamSF_Substitution_term <> N var
R12312:12315 LamSF_Terms <> lift def
R12319:12319 LamSF_Substitution_term <> M var
R12333:12336 LamSF_Terms <> lift def
R12341:12349 LamSF_Terms <> subst_rec def
R12355:12355 LamSF_Substitution_term <> n var
R12353:12353 LamSF_Substitution_term <> N var
R12351:12351 LamSF_Substitution_term <> M var
R12384:12387 LamSF_Terms <> lift def
R12400:12400 Coq.Init.Datatypes <> S constr
R12412:12412 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12400:12400 Coq.Init.Datatypes <> S constr
R12412:12412 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12434:12452 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R12434:12452 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R12434:12452 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R12434:12452 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
prf 12483:12501 <> subst_rec_lift_rec2
R12557:12559 Coq.Init.Logic <> :type_scope:x_'='_x not
R12517:12525 LamSF_Terms <> subst_rec def
R12556:12556 LamSF_Substitution_term <> n var
R12549:12551 LamSF_Terms <> Ref constr
R12528:12535 LamSF_Terms <> lift_rec def
R12540:12540 Coq.Init.Datatypes <> S constr
R12542:12542 LamSF_Substitution_term <> n var
R12537:12537 LamSF_Substitution_term <> M var
R12560:12560 LamSF_Substitution_term <> M var
R12603:12610 LamSF_Terms <> relocate def
R12619:12622 Test <> test def
R12625:12625 Coq.Init.Datatypes <> S constr
R12619:12622 Test <> test def
R12625:12625 Coq.Init.Datatypes <> S constr
R12677:12686 LamSF_Terms <> insert_Ref def
R12695:12701 Test <> compare def
R12695:12701 Test <> compare def
R12757:12760 LamSF_Terms <> lift def