forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LamSF_Tactics.glob
1314 lines (1314 loc) · 53.5 KB
/
LamSF_Tactics.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 021610f2eeaafa319c5abad3bbdb92df
FLamSF_Tactics
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2015 Test <> <> lib
R2034:2040 General <> <> lib
R2058:2068 LamSF_Terms <> <> lib
R2086:2090 Coq.omega.Omega <> <> lib
def 2105:2111 <> termred
R2121:2124 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2130:2133 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2125:2129 LamSF_Terms <> lamSF ind
R2116:2120 LamSF_Terms <> lamSF ind
def 2152:2159 <> preserve
R2166:2172 LamSF_Tactics <> termred def
R2185:2188 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2180:2184 LamSF_Terms <> lamSF ind
R2211:2215 LamSF_Terms <> lamSF ind
R2221:2224 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2236:2240 LamSF_Terms <> lamSF ind
R2248:2251 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2252:2252 LamSF_Tactics <> P var
R2254:2254 LamSF_Tactics <> y var
R2243:2243 LamSF_Tactics <> R var
R2247:2247 LamSF_Tactics <> y var
R2245:2245 LamSF_Tactics <> x var
R2218:2218 LamSF_Tactics <> P var
R2220:2220 LamSF_Tactics <> x var
ind 2269:2278 <> multi_step
constr 2308:2315 <> zero_red
constr 2356:2363 <> succ_red
R2289:2292 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2293:2299 LamSF_Tactics <> termred def
R2282:2288 LamSF_Tactics <> termred def
R2333:2342 LamSF_Tactics <> multi_step ind
R2350:2350 LamSF_Tactics <> M var
R2348:2348 LamSF_Tactics <> M var
R2344:2346 LamSF_Tactics <> red var
R2385:2387 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2393:2396 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2388:2392 LamSF_Terms <> lamSF ind
R2380:2384 LamSF_Terms <> lamSF ind
R2437:2440 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2459:2462 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2463:2472 LamSF_Tactics <> multi_step ind
R2480:2480 LamSF_Tactics <> P var
R2478:2478 LamSF_Tactics <> M var
R2474:2476 LamSF_Tactics <> red var
R2441:2450 LamSF_Tactics <> multi_step ind
R2458:2458 LamSF_Tactics <> P var
R2456:2456 LamSF_Tactics <> N var
R2452:2454 LamSF_Tactics <> red var
R2430:2432 LamSF_Tactics <> red var
R2436:2436 LamSF_Tactics <> N var
R2434:2434 LamSF_Tactics <> M var
ind 2495:2504 <> sequential
constr 2545:2551 <> seq_red
R2515:2518 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2526:2529 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2530:2536 LamSF_Tactics <> termred def
R2519:2525 LamSF_Tactics <> termred def
R2508:2514 LamSF_Tactics <> termred def
R2575:2581 LamSF_Tactics <> termred def
R2616:2619 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2628:2631 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2632:2641 LamSF_Tactics <> sequential ind
R2655:2655 LamSF_Tactics <> P var
R2653:2653 LamSF_Tactics <> M var
R2648:2651 LamSF_Tactics <> red2 var
R2643:2646 LamSF_Tactics <> red1 var
R2620:2623 LamSF_Tactics <> red2 var
R2627:2627 LamSF_Tactics <> P var
R2625:2625 LamSF_Tactics <> N var
R2608:2611 LamSF_Tactics <> red1 var
R2615:2615 LamSF_Tactics <> N var
R2613:2613 LamSF_Tactics <> M var
def 2712:2721 <> reflective
R2741:2745 LamSF_Terms <> lamSF ind
R2749:2751 LamSF_Tactics <> red var
R2755:2755 LamSF_Tactics <> M var
R2753:2753 LamSF_Tactics <> M var
prf 2765:2779 <> refl_multi_step
R2796:2802 LamSF_Tactics <> termred def
R2806:2815 LamSF_Tactics <> reflective def
R2818:2827 LamSF_Tactics <> multi_step ind
R2829:2831 LamSF_Tactics <> red var
prf 2870:2877 <> refl_seq
R2900:2906 LamSF_Tactics <> termred def
R2944:2947 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2963:2966 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2967:2976 LamSF_Tactics <> reflective def
R2978:2987 LamSF_Tactics <> sequential ind
R2994:2997 LamSF_Tactics <> red2 var
R2989:2992 LamSF_Tactics <> red1 var
R2948:2957 LamSF_Tactics <> reflective def
R2959:2962 LamSF_Tactics <> red2 var
R2929:2938 LamSF_Tactics <> reflective def
R2940:2943 LamSF_Tactics <> red1 var
R3032:3038 LamSF_Tactics <> seq_red constr
R3086:3095 LamSF_Tactics <> reflective def
R3098:3107 LamSF_Tactics <> multi_step ind
R3086:3095 LamSF_Tactics <> reflective def
R3098:3107 LamSF_Tactics <> multi_step ind
R3144:3153 LamSF_Tactics <> multi_step ind
R3144:3153 LamSF_Tactics <> multi_step ind
R3199:3208 LamSF_Tactics <> reflective def
R3211:3220 LamSF_Tactics <> sequential ind
R3199:3208 LamSF_Tactics <> reflective def
R3211:3220 LamSF_Tactics <> sequential ind
R3260:3269 LamSF_Tactics <> sequential ind
R3260:3269 LamSF_Tactics <> sequential ind
R3369:3378 LamSF_Tactics <> multi_step ind
R3369:3378 LamSF_Tactics <> multi_step ind
R3396:3403 LamSF_Tactics <> succ_red constr
R3483:3492 LamSF_Tactics <> sequential ind
R3483:3492 LamSF_Tactics <> sequential ind
R3513:3519 LamSF_Tactics <> seq_red constr
R3591:3600 LamSF_Tactics <> sequential ind
R3591:3600 LamSF_Tactics <> sequential ind
R3621:3627 LamSF_Tactics <> seq_red constr
def 3674:3683 <> transitive
R3707:3711 LamSF_Terms <> lamSF ind
R3722:3725 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3733:3736 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3737:3739 LamSF_Tactics <> red var
R3743:3743 LamSF_Tactics <> P var
R3741:3741 LamSF_Tactics <> M var
R3726:3728 LamSF_Tactics <> red var
R3732:3732 LamSF_Tactics <> P var
R3730:3730 LamSF_Tactics <> N var
R3715:3717 LamSF_Tactics <> red var
R3721:3721 LamSF_Tactics <> N var
R3719:3719 LamSF_Tactics <> M var
prf 3754:3767 <> transitive_red
R3783:3792 LamSF_Tactics <> transitive def
R3795:3804 LamSF_Tactics <> multi_step ind
R3806:3808 LamSF_Tactics <> red var
R3856:3863 LamSF_Tactics <> succ_red constr
R3856:3863 LamSF_Tactics <> succ_red constr
def 3898:3910 <> preserves_abs
R3919:3925 LamSF_Tactics <> termred def
R3951:3954 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3955:3957 LamSF_Tactics <> red var
R3968:3970 LamSF_Terms <> Abs constr
R3972:3972 LamSF_Tactics <> N var
R3960:3962 LamSF_Terms <> Abs constr
R3964:3964 LamSF_Tactics <> M var
R3944:3946 LamSF_Tactics <> red var
R3950:3950 LamSF_Tactics <> N var
R3948:3948 LamSF_Tactics <> M var
def 3988:4000 <> preserves_app
R4009:4015 LamSF_Tactics <> termred def
R4048:4051 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4060:4063 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4064:4066 LamSF_Tactics <> red var
R4079:4081 LamSF_Terms <> App constr
R4086:4087 LamSF_Tactics <> N' var
R4083:4084 LamSF_Tactics <> M' var
R4069:4071 LamSF_Terms <> App constr
R4075:4075 LamSF_Tactics <> N var
R4073:4073 LamSF_Tactics <> M var
R4052:4054 LamSF_Tactics <> red var
R4058:4059 LamSF_Tactics <> N' var
R4056:4056 LamSF_Tactics <> N var
R4040:4042 LamSF_Tactics <> red var
R4046:4047 LamSF_Tactics <> M' var
R4044:4044 LamSF_Tactics <> M var
prf 4098:4121 <> preserves_abs_multi_step
R4154:4157 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4158:4170 LamSF_Tactics <> preserves_abs def
R4173:4182 LamSF_Tactics <> multi_step ind
R4184:4186 LamSF_Tactics <> red var
R4137:4149 LamSF_Tactics <> preserves_abs def
R4151:4153 LamSF_Tactics <> red var
R4248:4250 LamSF_Terms <> Abs constr
R4233:4240 LamSF_Tactics <> succ_red constr
R4248:4250 LamSF_Terms <> Abs constr
R4233:4240 LamSF_Tactics <> succ_red constr
prf 4274:4297 <> preserves_app_multi_step
R4314:4320 LamSF_Tactics <> termred def
R4338:4341 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4359:4362 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4363:4375 LamSF_Tactics <> preserves_app def
R4378:4387 LamSF_Tactics <> multi_step ind
R4389:4391 LamSF_Tactics <> red var
R4342:4354 LamSF_Tactics <> preserves_app def
R4356:4358 LamSF_Tactics <> red var
R4324:4333 LamSF_Tactics <> reflective def
R4335:4337 LamSF_Tactics <> red var
R4492:4494 LamSF_Terms <> App constr
R4477:4484 LamSF_Tactics <> succ_red constr
R4492:4494 LamSF_Terms <> App constr
R4477:4484 LamSF_Tactics <> succ_red constr
R4516:4525 LamSF_Tactics <> transitive def
R4528:4537 LamSF_Tactics <> multi_step ind
R4516:4525 LamSF_Tactics <> transitive def
R4528:4537 LamSF_Tactics <> multi_step ind
R4556:4569 LamSF_Tactics <> transitive_red thm
R4589:4591 LamSF_Terms <> App constr
R4589:4591 LamSF_Terms <> App constr
prf 4630:4646 <> preserves_abs_seq
R4669:4675 LamSF_Tactics <> termred def
R4697:4700 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4719:4722 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4723:4735 LamSF_Tactics <> preserves_abs def
R4738:4747 LamSF_Tactics <> sequential ind
R4754:4757 LamSF_Tactics <> red2 var
R4749:4752 LamSF_Tactics <> red1 var
R4701:4713 LamSF_Tactics <> preserves_abs def
R4715:4718 LamSF_Tactics <> red2 var
R4679:4691 LamSF_Tactics <> preserves_abs def
R4693:4696 LamSF_Tactics <> red1 var
R4819:4821 LamSF_Terms <> Abs constr
R4805:4811 LamSF_Tactics <> seq_red constr
R4819:4821 LamSF_Terms <> Abs constr
R4805:4811 LamSF_Tactics <> seq_red constr
prf 4846:4862 <> preserves_app_seq
R4885:4891 LamSF_Tactics <> termred def
R4913:4916 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4935:4938 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4939:4951 LamSF_Tactics <> preserves_app def
R4954:4963 LamSF_Tactics <> sequential ind
R4970:4973 LamSF_Tactics <> red2 var
R4965:4968 LamSF_Tactics <> red1 var
R4917:4929 LamSF_Tactics <> preserves_app def
R4931:4934 LamSF_Tactics <> red2 var
R4895:4907 LamSF_Tactics <> preserves_app def
R4909:4912 LamSF_Tactics <> red1 var
R5050:5052 LamSF_Terms <> App constr
R5036:5042 LamSF_Tactics <> seq_red constr
R5050:5052 LamSF_Terms <> App constr
R5036:5042 LamSF_Tactics <> seq_red constr
def 5190:5203 <> preserves_abs1
R5211:5217 LamSF_Tactics <> termred def
R5242:5245 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5267:5273 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5274:5280 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5283:5284 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5294:5297 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5285:5287 LamSF_Tactics <> red var
R5292:5293 LamSF_Tactics <> N0 var
R5289:5290 LamSF_Tactics <> M0 var
R5304:5306 Coq.Init.Logic <> :type_scope:x_'='_x not
R5298:5300 LamSF_Terms <> Abs constr
R5302:5303 LamSF_Tactics <> N0 var
R5307:5307 LamSF_Tactics <> N var
R5258:5260 Coq.Init.Logic <> :type_scope:x_'='_x not
R5257:5257 LamSF_Tactics <> M var
R5261:5263 LamSF_Terms <> Abs constr
R5265:5266 LamSF_Tactics <> M0 var
R5235:5237 LamSF_Tactics <> red var
R5241:5241 LamSF_Tactics <> N var
R5239:5239 LamSF_Tactics <> M var
prf 5317:5341 <> preserves_abs1_multi_step
R5375:5378 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5379:5392 LamSF_Tactics <> preserves_abs1 def
R5395:5404 LamSF_Tactics <> multi_step ind
R5406:5408 LamSF_Tactics <> red var
R5357:5370 LamSF_Tactics <> preserves_abs1 def
R5372:5374 LamSF_Tactics <> red var
R5427:5440 LamSF_Tactics <> preserves_abs1 def
R5487:5493 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5504:5505 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5499:5503 LamSF_Terms <> lamSF ind
R5515:5518 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5513:5514 LamSF_Tactics <> N0 var
R5525:5527 Coq.Init.Logic <> :type_scope:x_'='_x not
R5519:5521 LamSF_Terms <> Abs constr
R5523:5524 LamSF_Tactics <> N0 var
R5487:5493 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5504:5505 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5499:5503 LamSF_Terms <> lamSF ind
R5515:5518 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5513:5514 LamSF_Tactics <> N0 var
R5525:5527 Coq.Init.Logic <> :type_scope:x_'='_x not
R5519:5521 LamSF_Terms <> Abs constr
R5523:5524 LamSF_Tactics <> N0 var
R5563:5569 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5580:5581 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5575:5579 LamSF_Terms <> lamSF ind
R5601:5604 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5582:5591 LamSF_Tactics <> multi_step ind
R5599:5600 LamSF_Tactics <> N0 var
R5611:5613 Coq.Init.Logic <> :type_scope:x_'='_x not
R5605:5607 LamSF_Terms <> Abs constr
R5609:5610 LamSF_Tactics <> N0 var
R5563:5569 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5580:5581 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5575:5579 LamSF_Terms <> lamSF ind
R5601:5604 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5582:5591 LamSF_Tactics <> multi_step ind
R5599:5600 LamSF_Tactics <> N0 var
R5611:5613 Coq.Init.Logic <> :type_scope:x_'='_x not
R5605:5607 LamSF_Terms <> Abs constr
R5609:5610 LamSF_Tactics <> N0 var
R5670:5677 LamSF_Tactics <> succ_red constr
R5670:5677 LamSF_Tactics <> succ_red constr
prf 5705:5722 <> preserves_abs1_seq
R5758:5761 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5794:5797 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5798:5811 LamSF_Tactics <> preserves_abs1 def
R5814:5823 LamSF_Tactics <> sequential ind
R5830:5833 LamSF_Tactics <> red2 var
R5825:5828 LamSF_Tactics <> red1 var
R5775:5788 LamSF_Tactics <> preserves_abs1 def
R5790:5793 LamSF_Tactics <> red2 var
R5739:5752 LamSF_Tactics <> preserves_abs1 def
R5754:5757 LamSF_Tactics <> red1 var
R5852:5865 LamSF_Tactics <> preserves_abs1 def
R5972:5978 LamSF_Tactics <> seq_red constr
R5972:5978 LamSF_Tactics <> seq_red constr
def 6071:6088 <> lift_rec_preserves
R6096:6102 LamSF_Tactics <> termred def
R6123:6127 LamSF_Terms <> lamSF ind
R6138:6141 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6156:6158 Coq.Init.Datatypes <> nat ind
R6162:6164 LamSF_Tactics <> red var
R6185:6192 LamSF_Terms <> lift_rec def
R6198:6198 LamSF_Tactics <> k var
R6196:6196 LamSF_Tactics <> n var
R6194:6194 LamSF_Tactics <> N var
R6168:6175 LamSF_Terms <> lift_rec def
R6181:6181 LamSF_Tactics <> k var
R6179:6179 LamSF_Tactics <> n var
R6177:6177 LamSF_Tactics <> M var
R6131:6133 LamSF_Tactics <> red var
R6137:6137 LamSF_Tactics <> N var
R6135:6135 LamSF_Tactics <> M var
prf 6210:6238 <> lift_rec_preserves_multi_step
R6277:6280 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6281:6298 LamSF_Tactics <> lift_rec_preserves def
R6301:6310 LamSF_Tactics <> multi_step ind
R6312:6314 LamSF_Tactics <> red var
R6255:6272 LamSF_Tactics <> lift_rec_preserves def
R6274:6276 LamSF_Tactics <> red var
R6333:6350 LamSF_Tactics <> lift_rec_preserves def
R6400:6407 LamSF_Terms <> lift_rec def
R6385:6392 LamSF_Tactics <> succ_red constr
R6400:6407 LamSF_Terms <> lift_rec def
R6385:6392 LamSF_Tactics <> succ_red constr
prf 6435:6456 <> lift_rec_preserves_seq
R6502:6505 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6529:6551 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6552:6569 LamSF_Tactics <> lift_rec_preserves def
R6572:6581 LamSF_Tactics <> sequential ind
R6588:6591 LamSF_Tactics <> red2 var
R6583:6586 LamSF_Tactics <> red1 var
R6506:6523 LamSF_Tactics <> lift_rec_preserves def
R6525:6528 LamSF_Tactics <> red2 var
R6479:6496 LamSF_Tactics <> lift_rec_preserves def
R6498:6501 LamSF_Tactics <> red1 var
R6615:6632 LamSF_Tactics <> lift_rec_preserves def
R6682:6689 LamSF_Terms <> lift_rec def
R6668:6674 LamSF_Tactics <> seq_red constr
R6682:6689 LamSF_Terms <> lift_rec def
R6668:6674 LamSF_Tactics <> seq_red constr
def 6794:6811 <> preserves_lift_rec
R6824:6828 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6834:6837 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6829:6833 LamSF_Terms <> lamSF ind
R6819:6823 LamSF_Terms <> lamSF ind
R6867:6870 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6905:6908 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6909:6915 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6918:6919 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6929:6932 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6920:6922 LamSF_Tactics <> red var
R6927:6928 LamSF_Tactics <> N0 var
R6924:6925 LamSF_Tactics <> M0 var
R6948:6950 Coq.Init.Logic <> :type_scope:x_'='_x not
R6933:6940 LamSF_Terms <> lift_rec def
R6947:6947 LamSF_Tactics <> k var
R6945:6945 LamSF_Tactics <> n var
R6942:6943 LamSF_Tactics <> N0 var
R6951:6951 LamSF_Tactics <> N var
R6901:6903 Coq.Init.Logic <> :type_scope:x_'='_x not
R6886:6893 LamSF_Terms <> lift_rec def
R6900:6900 LamSF_Tactics <> k var
R6898:6898 LamSF_Tactics <> n var
R6895:6896 LamSF_Tactics <> M0 var
R6904:6904 LamSF_Tactics <> M var
R6860:6862 LamSF_Tactics <> red var
R6866:6866 LamSF_Tactics <> N var
R6864:6864 LamSF_Tactics <> M var
prf 6962:6990 <> preserves_lift_rec_multi_step
R7029:7032 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7033:7050 LamSF_Tactics <> preserves_lift_rec def
R7053:7062 LamSF_Tactics <> multi_step ind
R7064:7066 LamSF_Tactics <> red var
R7007:7024 LamSF_Tactics <> preserves_lift_rec def
R7026:7028 LamSF_Tactics <> red var
R7084:7101 LamSF_Tactics <> preserves_lift_rec def
R7229:7236 LamSF_Tactics <> succ_red constr
R7229:7236 LamSF_Tactics <> succ_red constr
prf 7265:7286 <> preserves_lift_rec_seq
R7327:7330 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7367:7424 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7425:7442 LamSF_Tactics <> preserves_lift_rec def
R7445:7454 LamSF_Tactics <> sequential ind
R7461:7464 LamSF_Tactics <> red2 var
R7456:7459 LamSF_Tactics <> red1 var
R7344:7361 LamSF_Tactics <> preserves_lift_rec def
R7363:7366 LamSF_Tactics <> red2 var
R7304:7321 LamSF_Tactics <> preserves_lift_rec def
R7323:7326 LamSF_Tactics <> red1 var
R7482:7499 LamSF_Tactics <> preserves_lift_rec def
R7611:7617 LamSF_Tactics <> seq_red constr
R7611:7617 LamSF_Tactics <> seq_red constr
R7703:7706 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7699:7701 Coq.Init.Logic <> :type_scope:x_'='_x not
R7703:7706 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7699:7701 Coq.Init.Logic <> :type_scope:x_'='_x not
R7833:7835 Coq.Init.Logic <> :type_scope:x_'='_x not
R7828:7830 LamSF_Terms <> Ref constr
R7836:7843 LamSF_Terms <> lift_rec def
R7833:7835 Coq.Init.Logic <> :type_scope:x_'='_x not
R7828:7830 LamSF_Terms <> Ref constr
R7836:7843 LamSF_Terms <> lift_rec def
R7901:7903 Coq.Init.Logic <> :type_scope:x_'='_x not
R7897:7898 LamSF_Terms <> Op constr
R7904:7911 LamSF_Terms <> lift_rec def
R7901:7903 Coq.Init.Logic <> :type_scope:x_'='_x not
R7897:7898 LamSF_Terms <> Op constr
R7904:7911 LamSF_Terms <> lift_rec def
R7972:7974 Coq.Init.Logic <> :type_scope:x_'='_x not
R7965:7967 LamSF_Terms <> App constr
R7975:7982 LamSF_Terms <> lift_rec def
R7972:7974 Coq.Init.Logic <> :type_scope:x_'='_x not
R7965:7967 LamSF_Terms <> App constr
R7975:7982 LamSF_Terms <> lift_rec def
R8040:8042 Coq.Init.Logic <> :type_scope:x_'='_x not
R8035:8037 LamSF_Terms <> Abs constr
R8043:8050 LamSF_Terms <> lift_rec def
R8040:8042 Coq.Init.Logic <> :type_scope:x_'='_x not
R8035:8037 LamSF_Terms <> Abs constr
R8043:8050 LamSF_Terms <> lift_rec def
R8118:8120 Coq.Init.Logic <> :type_scope:x_'='_x not
R8103:8110 LamSF_Terms <> lift_rec def
R8121:8123 LamSF_Terms <> Ref constr
R8118:8120 Coq.Init.Logic <> :type_scope:x_'='_x not
R8103:8110 LamSF_Terms <> lift_rec def
R8121:8123 LamSF_Terms <> Ref constr
R8186:8188 Coq.Init.Logic <> :type_scope:x_'='_x not
R8171:8178 LamSF_Terms <> lift_rec def
R8189:8190 LamSF_Terms <> Op constr
R8186:8188 Coq.Init.Logic <> :type_scope:x_'='_x not
R8171:8178 LamSF_Terms <> lift_rec def
R8189:8190 LamSF_Terms <> Op constr
R8253:8255 Coq.Init.Logic <> :type_scope:x_'='_x not
R8238:8245 LamSF_Terms <> lift_rec def
R8256:8258 LamSF_Terms <> App constr
R8253:8255 Coq.Init.Logic <> :type_scope:x_'='_x not
R8238:8245 LamSF_Terms <> lift_rec def
R8256:8258 LamSF_Terms <> App constr
R8323:8325 Coq.Init.Logic <> :type_scope:x_'='_x not
R8308:8315 LamSF_Terms <> lift_rec def
R8326:8328 LamSF_Terms <> Abs constr
R8323:8325 Coq.Init.Logic <> :type_scope:x_'='_x not
R8308:8315 LamSF_Terms <> lift_rec def
R8326:8328 LamSF_Terms <> Abs constr
R8455:8457 LamSF_Terms <> Ref constr
R8455:8457 LamSF_Terms <> Ref constr
R8513:8515 LamSF_Terms <> App constr
R8513:8515 LamSF_Terms <> App constr
R8573:8574 LamSF_Terms <> Op constr
R8573:8574 LamSF_Terms <> Op constr
R8629:8631 LamSF_Terms <> Abs constr
R8629:8631 LamSF_Terms <> Abs constr
def 8712:8722 <> implies_red
R8736:8742 LamSF_Tactics <> termred def
R8768:8771 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8772:8775 LamSF_Tactics <> red2 var
R8779:8779 LamSF_Tactics <> N var
R8777:8777 LamSF_Tactics <> M var
R8760:8763 LamSF_Tactics <> red1 var
R8767:8767 LamSF_Tactics <> N var
R8765:8765 LamSF_Tactics <> M var
prf 8790:8811 <> implies_red_multi_step
R8867:8919 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8920:8930 LamSF_Tactics <> implies_red def
R8951:8960 LamSF_Tactics <> multi_step ind
R8962:8965 LamSF_Tactics <> red2 var
R8933:8942 LamSF_Tactics <> multi_step ind
R8944:8947 LamSF_Tactics <> red1 var
R8832:8842 LamSF_Tactics <> implies_red def
R8851:8860 LamSF_Tactics <> multi_step ind
R8862:8865 LamSF_Tactics <> red2 var
R8844:8847 LamSF_Tactics <> red1 var
R9040:9053 LamSF_Tactics <> transitive_red thm
R9040:9053 LamSF_Tactics <> transitive_red thm
prf 9082:9096 <> implies_red_seq
R9162:9170 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9205:9211 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9212:9222 LamSF_Tactics <> implies_red def
R9248:9257 LamSF_Tactics <> multi_step ind
R9259:9262 LamSF_Tactics <> red3 var
R9225:9234 LamSF_Tactics <> sequential ind
R9241:9244 LamSF_Tactics <> red2 var
R9236:9239 LamSF_Tactics <> red1 var
R9171:9181 LamSF_Tactics <> implies_red def
R9189:9198 LamSF_Tactics <> multi_step ind
R9200:9203 LamSF_Tactics <> red3 var
R9183:9186 LamSF_Tactics <> red2 var
R9127:9137 LamSF_Tactics <> implies_red def
R9146:9155 LamSF_Tactics <> multi_step ind
R9157:9160 LamSF_Tactics <> red3 var
R9139:9142 LamSF_Tactics <> red1 var
R9311:9324 LamSF_Tactics <> transitive_red thm
R9311:9324 LamSF_Tactics <> transitive_red thm
def 9361:9381 <> subst_rec_preserves_l
R9389:9395 LamSF_Tactics <> termred def
R9419:9423 LamSF_Terms <> lamSF ind
R9435:9438 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9452:9454 Coq.Init.Datatypes <> nat ind
R9458:9460 LamSF_Tactics <> red var
R9482:9490 LamSF_Terms <> subst_rec def
R9497:9497 LamSF_Tactics <> k var
R9495:9495 LamSF_Tactics <> N var
R9492:9493 LamSF_Tactics <> M' var
R9464:9472 LamSF_Terms <> subst_rec def
R9478:9478 LamSF_Tactics <> k var
R9476:9476 LamSF_Tactics <> N var
R9474:9474 LamSF_Tactics <> M var
R9427:9429 LamSF_Tactics <> red var
R9433:9434 LamSF_Tactics <> M' var
R9431:9431 LamSF_Tactics <> M var
def 9513:9533 <> subst_rec_preserves_r
R9541:9547 LamSF_Tactics <> termred def
R9571:9575 LamSF_Terms <> lamSF ind
R9587:9590 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9604:9606 Coq.Init.Datatypes <> nat ind
R9610:9612 LamSF_Tactics <> red var
R9634:9642 LamSF_Terms <> subst_rec def
R9649:9649 LamSF_Tactics <> k var
R9646:9647 LamSF_Tactics <> N' var
R9644:9644 LamSF_Tactics <> M var
R9616:9624 LamSF_Terms <> subst_rec def
R9630:9630 LamSF_Tactics <> k var
R9628:9628 LamSF_Tactics <> N var
R9626:9626 LamSF_Tactics <> M var
R9579:9581 LamSF_Tactics <> red var
R9585:9586 LamSF_Tactics <> N' var
R9583:9583 LamSF_Tactics <> N var
def 9665:9683 <> subst_rec_preserves
R9691:9697 LamSF_Tactics <> termred def
R9719:9723 LamSF_Terms <> lamSF ind
R9735:9738 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9760:9763 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9777:9779 Coq.Init.Datatypes <> nat ind
R9783:9785 LamSF_Tactics <> red var
R9807:9815 LamSF_Terms <> subst_rec def
R9823:9823 LamSF_Tactics <> k var
R9820:9821 LamSF_Tactics <> N' var
R9817:9818 LamSF_Tactics <> M' var
R9789:9797 LamSF_Terms <> subst_rec def
R9803:9803 LamSF_Tactics <> k var
R9801:9801 LamSF_Tactics <> N var
R9799:9799 LamSF_Tactics <> M var
R9752:9754 LamSF_Tactics <> red var
R9758:9759 LamSF_Tactics <> N' var
R9756:9756 LamSF_Tactics <> N var
R9727:9729 LamSF_Tactics <> red var
R9733:9734 LamSF_Tactics <> M' var
R9731:9731 LamSF_Tactics <> M var
prf 9834:9865 <> subst_rec_preserves_l_multi_step
R9883:9889 LamSF_Tactics <> termred def
R9918:9921 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9922:9942 LamSF_Tactics <> subst_rec_preserves_l def
R9945:9954 LamSF_Tactics <> multi_step ind
R9956:9958 LamSF_Tactics <> red var
R9893:9913 LamSF_Tactics <> subst_rec_preserves_l def
R9915:9917 LamSF_Tactics <> red var
R9977:9997 LamSF_Tactics <> subst_rec_preserves_l def
R10049:10057 LamSF_Terms <> subst_rec def
R10034:10041 LamSF_Tactics <> succ_red constr
R10049:10057 LamSF_Terms <> subst_rec def
R10034:10041 LamSF_Tactics <> succ_red constr
prf 10086:10117 <> subst_rec_preserves_r_multi_step
R10135:10141 LamSF_Tactics <> termred def
R10170:10173 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10174:10194 LamSF_Tactics <> subst_rec_preserves_r def
R10197:10206 LamSF_Tactics <> multi_step ind
R10208:10210 LamSF_Tactics <> red var
R10145:10165 LamSF_Tactics <> subst_rec_preserves_r def
R10167:10169 LamSF_Tactics <> red var
R10229:10249 LamSF_Tactics <> subst_rec_preserves_r def
R10301:10309 LamSF_Terms <> subst_rec def
R10286:10293 LamSF_Tactics <> succ_red constr
R10301:10309 LamSF_Terms <> subst_rec def
R10286:10293 LamSF_Tactics <> succ_red constr
prf 10338:10367 <> subst_rec_preserves_multi_step
R10385:10391 LamSF_Tactics <> termred def
R10420:10423 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10449:10452 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10453:10471 LamSF_Tactics <> subst_rec_preserves def
R10474:10483 LamSF_Tactics <> multi_step ind
R10485:10487 LamSF_Tactics <> red var
R10424:10444 LamSF_Tactics <> subst_rec_preserves_r def
R10446:10448 LamSF_Tactics <> red var
R10395:10415 LamSF_Tactics <> subst_rec_preserves_l def
R10417:10419 LamSF_Tactics <> red var
R10507:10525 LamSF_Tactics <> subst_rec_preserves def
R10546:10555 LamSF_Tactics <> transitive def
R10558:10567 LamSF_Tactics <> multi_step ind
R10546:10555 LamSF_Tactics <> transitive def
R10558:10567 LamSF_Tactics <> multi_step ind
R10586:10599 LamSF_Tactics <> transitive_red thm
R10610:10619 LamSF_Tactics <> transitive def
R10642:10650 LamSF_Terms <> subst_rec def
R10642:10650 LamSF_Terms <> subst_rec def
R10676:10707 LamSF_Tactics <> subst_rec_preserves_l_multi_step thm
R10718:10749 LamSF_Tactics <> subst_rec_preserves_r_multi_step thm
prf 10766:10790 <> subst_rec_preserves_l_seq
R10835:10839 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10880:10933 Coq.Init.Logic <> :type_scope:x_'->'_x not
R10934:10954 LamSF_Tactics <> subst_rec_preserves_l def
R10957:10966 LamSF_Tactics <> sequential ind
R10973:10976 LamSF_Tactics <> red2 var
R10968:10971 LamSF_Tactics <> red1 var
R10854:10874 LamSF_Tactics <> subst_rec_preserves_l def
R10876:10879 LamSF_Tactics <> red2 var
R10809:10829 LamSF_Tactics <> subst_rec_preserves_l def
R10831:10834 LamSF_Tactics <> red1 var
R10995:11015 LamSF_Tactics <> subst_rec_preserves_l def
R11066:11074 LamSF_Terms <> subst_rec def
R11052:11058 LamSF_Tactics <> seq_red constr
R11066:11074 LamSF_Terms <> subst_rec def
R11052:11058 LamSF_Tactics <> seq_red constr
prf 11104:11128 <> subst_rec_preserves_r_seq
R11173:11177 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11218:11280 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11281:11301 LamSF_Tactics <> subst_rec_preserves_r def
R11304:11313 LamSF_Tactics <> sequential ind
R11320:11323 LamSF_Tactics <> red2 var
R11315:11318 LamSF_Tactics <> red1 var
R11192:11212 LamSF_Tactics <> subst_rec_preserves_r def
R11214:11217 LamSF_Tactics <> red2 var
R11147:11167 LamSF_Tactics <> subst_rec_preserves_r def
R11169:11172 LamSF_Tactics <> red1 var
R11342:11362 LamSF_Tactics <> subst_rec_preserves_r def
R11413:11421 LamSF_Terms <> subst_rec def
R11399:11405 LamSF_Tactics <> seq_red constr
R11413:11421 LamSF_Terms <> subst_rec def
R11399:11405 LamSF_Tactics <> seq_red constr
prf 11451:11473 <> subst_rec_preserves_seq
R11516:11520 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11559:11621 Coq.Init.Logic <> :type_scope:x_'->'_x not
R11622:11640 LamSF_Tactics <> subst_rec_preserves def
R11643:11652 LamSF_Tactics <> sequential ind
R11659:11662 LamSF_Tactics <> red2 var
R11654:11657 LamSF_Tactics <> red1 var
R11535:11553 LamSF_Tactics <> subst_rec_preserves def
R11555:11558 LamSF_Tactics <> red2 var
R11492:11510 LamSF_Tactics <> subst_rec_preserves def
R11512:11515 LamSF_Tactics <> red1 var
R11681:11699 LamSF_Tactics <> subst_rec_preserves def
R11765:11773 LamSF_Terms <> subst_rec def
R11751:11757 LamSF_Tactics <> seq_red constr
R11765:11773 LamSF_Terms <> subst_rec def
R11751:11757 LamSF_Tactics <> seq_red constr
R11980:11989 LamSF_Tactics <> multi_step ind
R11996:11998 LamSF_Terms <> App constr
R11980:11989 LamSF_Tactics <> multi_step ind
R11996:11998 LamSF_Terms <> App constr
R12050:12059 LamSF_Tactics <> multi_step ind
R12066:12068 LamSF_Terms <> Ref constr
R12050:12059 LamSF_Tactics <> multi_step ind
R12066:12068 LamSF_Terms <> Ref constr
R12118:12127 LamSF_Tactics <> multi_step ind
R12134:12135 LamSF_Terms <> Op constr
R12118:12127 LamSF_Tactics <> multi_step ind
R12134:12135 LamSF_Terms <> Op constr
R12185:12194 LamSF_Tactics <> multi_step ind
R12201:12203 LamSF_Terms <> Abs constr
R12185:12194 LamSF_Tactics <> multi_step ind
R12201:12203 LamSF_Terms <> Abs constr
R12258:12260 LamSF_Terms <> Ref constr
R12258:12260 LamSF_Terms <> Ref constr
R12315:12317 LamSF_Terms <> App constr
R12315:12317 LamSF_Terms <> App constr
R12374:12375 LamSF_Terms <> Op constr
R12374:12375 LamSF_Terms <> Op constr
R12430:12432 LamSF_Terms <> Abs constr
R12430:12432 LamSF_Terms <> Abs constr
R12482:12491 LamSF_Tactics <> multi_step ind
R12500:12502 LamSF_Terms <> Ref constr
R12482:12491 LamSF_Tactics <> multi_step ind
R12500:12502 LamSF_Terms <> Ref constr
R12550:12559 LamSF_Tactics <> multi_step ind
R12568:12570 LamSF_Terms <> App constr
R12550:12559 LamSF_Tactics <> multi_step ind
R12568:12570 LamSF_Terms <> App constr
R12620:12629 LamSF_Tactics <> multi_step ind
R12638:12639 LamSF_Terms <> Op constr
R12620:12629 LamSF_Tactics <> multi_step ind
R12638:12639 LamSF_Terms <> Op constr
R12687:12696 LamSF_Tactics <> multi_step ind
R12705:12707 LamSF_Terms <> Abs constr
R12687:12696 LamSF_Tactics <> multi_step ind
R12705:12707 LamSF_Terms <> Abs constr
R12762:12764 LamSF_Terms <> Ref constr
R12762:12764 LamSF_Terms <> Ref constr
R12819:12821 LamSF_Terms <> App constr
R12819:12821 LamSF_Terms <> App constr
R12878:12879 LamSF_Terms <> Op constr
R12878:12879 LamSF_Terms <> Op constr
R12934:12936 LamSF_Terms <> Abs constr
R12934:12936 LamSF_Terms <> Abs constr
R13000:13003 LamSF_Terms <> lift def
R12989:12992 LamSF_Terms <> lift def
R13000:13003 LamSF_Terms <> lift def
R12989:12992 LamSF_Terms <> lift def
R13020:13023 LamSF_Terms <> lift def
R13035:13052 LamSF_Tactics <> lift_rec_preserves def
def 13112:13118 <> diamond
R13133:13139 LamSF_Tactics <> termred def
R13166:13169 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13188:13191 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13192:13198 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13200:13201 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13210:13213 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13202:13205 LamSF_Tactics <> red2 var
R13209:13209 LamSF_Tactics <> Q var
R13207:13207 LamSF_Tactics <> N var
R13214:13217 LamSF_Tactics <> red1 var
R13221:13221 LamSF_Tactics <> Q var
R13219:13219 LamSF_Tactics <> P var
R13180:13183 LamSF_Tactics <> red2 var
R13187:13187 LamSF_Tactics <> P var
R13185:13185 LamSF_Tactics <> M var
R13158:13161 LamSF_Tactics <> red1 var
R13165:13165 LamSF_Tactics <> N var
R13163:13163 LamSF_Tactics <> M var
prf 13232:13243 <> diamond_flip
R13281:13284 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13285:13291 LamSF_Tactics <> diamond def
R13298:13301 LamSF_Tactics <> red1 var
R13293:13296 LamSF_Tactics <> red2 var
R13264:13270 LamSF_Tactics <> diamond def
R13277:13280 LamSF_Tactics <> red2 var
R13272:13275 LamSF_Tactics <> red1 var
R13319:13325 LamSF_Tactics <> diamond def
prf 13393:13405 <> diamond_strip
R13445:13448 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13449:13455 LamSF_Tactics <> diamond def
R13463:13472 LamSF_Tactics <> multi_step ind
R13474:13477 LamSF_Tactics <> red2 var
R13457:13460 LamSF_Tactics <> red1 var
R13428:13434 LamSF_Tactics <> diamond def
R13441:13444 LamSF_Tactics <> red2 var
R13436:13439 LamSF_Tactics <> red1 var
R13506:13517 LamSF_Tactics <> diamond_flip thm
R13643:13650 LamSF_Tactics <> succ_red constr
R13643:13650 LamSF_Tactics <> succ_red constr
def 13686:13697 <> diamond_star
R13711:13717 LamSF_Tactics <> termred def
R13744:13747 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13766:13772 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13773:13779 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13781:13782 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13791:13794 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13783:13786 LamSF_Tactics <> red1 var
R13790:13790 LamSF_Tactics <> Q var
R13788:13788 LamSF_Tactics <> P var
R13795:13804 LamSF_Tactics <> multi_step ind
R13813:13813 LamSF_Tactics <> Q var
R13811:13811 LamSF_Tactics <> N var
R13806:13809 LamSF_Tactics <> red2 var
R13758:13761 LamSF_Tactics <> red2 var
R13765:13765 LamSF_Tactics <> P var
R13763:13763 LamSF_Tactics <> M var
R13736:13739 LamSF_Tactics <> red1 var
R13743:13743 LamSF_Tactics <> N var
R13741:13741 LamSF_Tactics <> M var
prf 13824:13841 <> diamond_star_strip
R13884:13887 Coq.Init.Logic <> :type_scope:x_'->'_x not
R13888:13894 LamSF_Tactics <> diamond def
R13914:13917 LamSF_Tactics <> red1 var
R13897:13906 LamSF_Tactics <> multi_step ind
R13908:13911 LamSF_Tactics <> red2 var
R13862:13873 LamSF_Tactics <> diamond_star def
R13880:13883 LamSF_Tactics <> red2 var
R13875:13878 LamSF_Tactics <> red1 var
R14054:14067 LamSF_Tactics <> transitive_red thm
R14054:14067 LamSF_Tactics <> transitive_red thm
prf 14097:14110 <> diamond_tiling
R14150:14153 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14154:14160 LamSF_Tactics <> diamond def
R14181:14190 LamSF_Tactics <> multi_step ind
R14192:14195 LamSF_Tactics <> red2 var
R14163:14172 LamSF_Tactics <> multi_step ind
R14174:14177 LamSF_Tactics <> red1 var
R14133:14139 LamSF_Tactics <> diamond def
R14146:14149 LamSF_Tactics <> red2 var
R14141:14144 LamSF_Tactics <> red1 var
R14251:14263 LamSF_Tactics <> diamond_strip thm
R14251:14263 LamSF_Tactics <> diamond_strip thm
R14353:14360 LamSF_Tactics <> succ_red constr
R14353:14360 LamSF_Tactics <> succ_red constr
prf 14420:14430 <> diamond_seq
R14471:14474 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14491:14494 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14495:14501 LamSF_Tactics <> diamond def
R14508:14517 LamSF_Tactics <> sequential ind
R14524:14527 LamSF_Tactics <> red2 var
R14519:14522 LamSF_Tactics <> red1 var
R14503:14505 LamSF_Tactics <> red var
R14475:14481 LamSF_Tactics <> diamond def
R14487:14490 LamSF_Tactics <> red2 var
R14483:14485 LamSF_Tactics <> red var
R14455:14461 LamSF_Tactics <> diamond def
R14467:14470 LamSF_Tactics <> red1 var
R14463:14465 LamSF_Tactics <> red var
R14546:14552 LamSF_Tactics <> diamond def
R14661:14667 LamSF_Tactics <> seq_red constr
R14661:14667 LamSF_Tactics <> seq_red constr
prf 14696:14708 <> relocate_null
R14727:14729 Coq.Init.Datatypes <> nat ind
R14748:14750 Coq.Init.Logic <> :type_scope:x_'='_x not
R14733:14740 LamSF_Terms <> relocate def
R14744:14745 LamSF_Tactics <> n0 var
R14742:14742 LamSF_Tactics <> n var
R14751:14751 LamSF_Tactics <> n var
R14779:14786 LamSF_Terms <> relocate def
R14795:14798 Test <> test def
R14795:14798 Test <> test def
prf 14843:14859 <> relocate_lessthan
R14881:14884 Coq.Init.Logic <> :type_scope:x_'->'_x not
R14899:14902 Coq.Init.Logic <> :type_scope:x_'='_x not
R14906:14906 Coq.Init.Logic <> :type_scope:x_'='_x not
R14885:14892 LamSF_Terms <> relocate def
R14898:14898 LamSF_Tactics <> n var
R14896:14896 LamSF_Tactics <> m var
R14894:14894 LamSF_Tactics <> k var
R14904:14904 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R14903:14903 LamSF_Tactics <> n var
R14905:14905 LamSF_Tactics <> k var
R14878:14879 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R14877:14877 LamSF_Tactics <> m var
R14880:14880 LamSF_Tactics <> k var
R14935:14942 LamSF_Terms <> relocate def
R14950:14953 Test <> test def
R14950:14953 Test <> test def
prf 14995:15014 <> relocate_greaterthan
R15035:15038 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15053:15055 Coq.Init.Logic <> :type_scope:x_'='_x not
R15039:15046 LamSF_Terms <> relocate def
R15052:15052 LamSF_Tactics <> n var
R15050:15050 LamSF_Tactics <> m var
R15048:15048 LamSF_Tactics <> k var
R15056:15056 LamSF_Tactics <> k var
R15033:15033 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R15032:15032 LamSF_Tactics <> m var
R15034:15034 LamSF_Tactics <> k var
R15085:15092 LamSF_Terms <> relocate def
R15100:15103 Test <> test def
R15100:15103 Test <> test def
R15174:15190 LamSF_Tactics <> relocate_lessthan thm
R15232:15251 LamSF_Tactics <> relocate_greaterthan thm
R15291:15303 LamSF_Tactics <> relocate_null thm
prf 15316:15333 <> relocate_zero_succ
R15367:15369 Coq.Init.Logic <> :type_scope:x_'='_x not
R15349:15356 LamSF_Terms <> relocate def
R15366:15366 LamSF_Tactics <> k var
R15361:15361 Coq.Init.Datatypes <> S constr
R15363:15363 LamSF_Tactics <> n var
prf 15404:15416 <> relocate_succ
R15458:15460 Coq.Init.Logic <> :type_scope:x_'='_x not
R15435:15442 LamSF_Terms <> relocate def
R15457:15457 LamSF_Tactics <> k var
R15451:15451 Coq.Init.Datatypes <> S constr
R15453:15454 LamSF_Tactics <> n0 var
R15445:15445 Coq.Init.Datatypes <> S constr
R15447:15447 LamSF_Tactics <> n var
R15461:15461 Coq.Init.Datatypes <> S constr
R15463:15470 LamSF_Terms <> relocate def
R15477:15477 LamSF_Tactics <> k var
R15474:15475 LamSF_Tactics <> n0 var
R15472:15472 LamSF_Tactics <> n var
R15504:15511 LamSF_Terms <> relocate def
R15519:15522 Test <> test def
R15531:15531 Coq.Init.Datatypes <> S constr
R15524:15524 Coq.Init.Datatypes <> S constr
R15543:15546 Test <> test def
R15519:15522 Test <> test def
R15531:15531 Coq.Init.Datatypes <> S constr
R15524:15524 Coq.Init.Datatypes <> S constr
R15543:15546 Test <> test def
R15543:15546 Test <> test def
prf 15596:15608 <> relocate_mono
R15659:15662 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15664:15664 Coq.Init.Logic <> :type_scope:x_'='_x not
R15663:15663 LamSF_Tactics <> M var
R15665:15665 LamSF_Tactics <> N var
R15642:15644 Coq.Init.Logic <> :type_scope:x_'='_x not
R15628:15635 LamSF_Terms <> relocate def
R15641:15641 LamSF_Tactics <> k var
R15639:15639 LamSF_Tactics <> n var
R15637:15637 LamSF_Tactics <> M var
R15645:15652 LamSF_Terms <> relocate def
R15658:15658 LamSF_Tactics <> k var
R15656:15656 LamSF_Tactics <> n var
R15654:15654 LamSF_Tactics <> N var
R15701:15708 LamSF_Terms <> relocate def
R15716:15719 Test <> test def
R15732:15735 Test <> test def
R15716:15719 Test <> test def
R15732:15735 Test <> test def
R15732:15735 Test <> test def
prf 15775:15787 <> lift_rec_mono
R15838:15841 Coq.Init.Logic <> :type_scope:x_'->'_x not
R15843:15843 Coq.Init.Logic <> :type_scope:x_'='_x not
R15842:15842 LamSF_Tactics <> M var
R15844:15844 LamSF_Tactics <> N var
R15821:15823 Coq.Init.Logic <> :type_scope:x_'='_x not
R15807:15814 LamSF_Terms <> lift_rec def
R15820:15820 LamSF_Tactics <> k var
R15818:15818 LamSF_Tactics <> n var
R15816:15816 LamSF_Tactics <> M var
R15824:15831 LamSF_Terms <> lift_rec def
R15837:15837 LamSF_Tactics <> k var
R15835:15835 LamSF_Tactics <> n var
R15833:15833 LamSF_Tactics <> N var
R15909:15909 Coq.Init.Logic <> :type_scope:x_'='_x not
R15909:15909 Coq.Init.Logic <> :type_scope:x_'='_x not
R15925:15937 LamSF_Tactics <> relocate_mono thm
R16001:16003 Coq.Init.Logic <> :type_scope:x_'='_x not
R16001:16003 Coq.Init.Logic <> :type_scope:x_'='_x not
R16065:16067 Coq.Init.Logic <> :type_scope:x_'='_x not
R16065:16067 Coq.Init.Logic <> :type_scope:x_'='_x not
R16098:16100 Coq.Init.Logic <> :type_scope:x_'='_x not
R16098:16100 Coq.Init.Logic <> :type_scope:x_'='_x not
prf 16150:16162 <> insert_Ref_lt
R16184:16187 Coq.Init.Logic <> :type_scope:x_'->'_x not
R16204:16206 Coq.Init.Logic <> :type_scope:x_'='_x not
R16188:16197 LamSF_Terms <> insert_Ref def
R16203:16203 LamSF_Tactics <> k var
R16201:16201 LamSF_Tactics <> n var
R16199:16199 LamSF_Tactics <> M var
R16207:16209 LamSF_Terms <> Ref constr
R16211:16211 LamSF_Tactics <> n var
R16181:16182 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R16180:16180 LamSF_Tactics <> n var
R16183:16183 LamSF_Tactics <> k var
R16241:16250 LamSF_Terms <> insert_Ref def
R16271:16277 Test <> compare def
R16271:16277 Test <> compare def
R16335:16341 Test <> compare def
R16335:16341 Test <> compare def
R16398:16404 Test <> compare def
R16398:16404 Test <> compare def
R16461:16467 Test <> compare def
R16461:16467 Test <> compare def
prf 16531:16543 <> insert_Ref_eq
R16565:16568 Coq.Init.Logic <> :type_scope:x_'->'_x not
R16585:16587 Coq.Init.Logic <> :type_scope:x_'='_x not
R16569:16578 LamSF_Terms <> insert_Ref def
R16584:16584 LamSF_Tactics <> k var
R16582:16582 LamSF_Tactics <> n var
R16580:16580 LamSF_Tactics <> M var
R16588:16591 LamSF_Terms <> lift def
R16595:16595 LamSF_Tactics <> M var
R16593:16593 LamSF_Tactics <> k var
R16562:16563 Coq.Init.Logic <> :type_scope:x_'='_x not
R16561:16561 LamSF_Tactics <> n var
R16564:16564 LamSF_Tactics <> k var
R16625:16634 LamSF_Terms <> insert_Ref def
R16655:16661 Test <> compare def
R16655:16661 Test <> compare def
R16720:16723 LamSF_Terms <> lift def
R16733:16740 LamSF_Terms <> lift_rec def
R16750:16757 LamSF_Terms <> relocate def
R16765:16768 Test <> test def
R16765:16768 Test <> test def
R16805:16811 Test <> compare def
R16805:16811 Test <> compare def
R16869:16872 LamSF_Terms <> lift def
R16882:16889 LamSF_Terms <> lift_rec def
R16899:16906 LamSF_Terms <> relocate def
R16914:16917 Test <> test def
R16914:16917 Test <> test def
R16954:16960 Test <> compare def
R16954:16960 Test <> compare def
R17025:17031 Test <> compare def
R17025:17031 Test <> compare def
prf 17104:17116 <> insert_Ref_gt
R17138:17141 Coq.Init.Logic <> :type_scope:x_'->'_x not
R17158:17160 Coq.Init.Logic <> :type_scope:x_'='_x not
R17142:17151 LamSF_Terms <> insert_Ref def
R17157:17157 LamSF_Tactics <> k var
R17155:17155 LamSF_Tactics <> n var
R17153:17153 LamSF_Tactics <> M var
R17161:17163 LamSF_Terms <> Ref constr
R17166:17169 Coq.Init.Peano <> pred syndef
R17171:17171 LamSF_Tactics <> n var
R17135:17136 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R17134:17134 LamSF_Tactics <> n var
R17137:17137 LamSF_Tactics <> k var
R17202:17211 LamSF_Terms <> insert_Ref def
R17232:17238 Test <> compare def
R17232:17238 Test <> compare def