-
Notifications
You must be signed in to change notification settings - Fork 1
/
untypedLC.glob
2284 lines (2284 loc) · 85.9 KB
/
untypedLC.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 42ffc0235c212b9ddd22aa161c42212f
FuntypedLC
R15:17 Coq.Init.Nat <> <> lib
R35:38 Coq.Lists.List <> <> lib
ind 492:497 <> letter
constr 512:512 <> a
constr 519:519 <> b
constr 526:526 <> c
constr 533:533 <> d
constr 540:540 <> e
constr 547:547 <> f
constr 553:553 <> g
constr 560:560 <> h
constr 567:567 <> i
constr 574:574 <> j
constr 581:581 <> k
constr 588:588 <> l
constr 594:594 <> m
constr 601:601 <> n
constr 608:608 <> o
constr 615:615 <> p
constr 622:622 <> q
constr 629:629 <> r
constr 635:635 <> s
constr 642:642 <> t
constr 649:649 <> u
constr 656:656 <> v
constr 663:663 <> w
constr 670:670 <> x
constr 676:676 <> y
constr 683:683 <> z
constr 689:690 <> a1
constr 696:697 <> b1
constr 703:704 <> c1
constr 710:711 <> d1
constr 717:718 <> e1
constr 724:725 <> f1
constr 731:732 <> g1
constr 738:739 <> h1
constr 745:746 <> i1
constr 752:753 <> j1
constr 759:760 <> k1
constr 766:767 <> l1
constr 773:774 <> m1
constr 780:781 <> n1
constr 787:788 <> o1
constr 794:795 <> p1
constr 801:802 <> q1
constr 808:809 <> r1
constr 815:816 <> s1
constr 822:823 <> t1
constr 829:830 <> u1
constr 836:837 <> v1
constr 843:844 <> w1
constr 850:851 <> x1
constr 857:858 <> y1
constr 864:865 <> z1
R513:513 untypedLC <> letter ind
R520:520 untypedLC <> letter ind
R527:527 untypedLC <> letter ind
R534:534 untypedLC <> letter ind
R541:541 untypedLC <> letter ind
R548:548 untypedLC <> letter ind
R554:554 untypedLC <> letter ind
R561:561 untypedLC <> letter ind
R568:568 untypedLC <> letter ind
R575:575 untypedLC <> letter ind
R582:582 untypedLC <> letter ind
R589:589 untypedLC <> letter ind
R595:595 untypedLC <> letter ind
R602:602 untypedLC <> letter ind
R609:609 untypedLC <> letter ind
R616:616 untypedLC <> letter ind
R623:623 untypedLC <> letter ind
R630:630 untypedLC <> letter ind
R636:636 untypedLC <> letter ind
R643:643 untypedLC <> letter ind
R650:650 untypedLC <> letter ind
R657:657 untypedLC <> letter ind
R664:664 untypedLC <> letter ind
R671:671 untypedLC <> letter ind
R677:677 untypedLC <> letter ind
R684:684 untypedLC <> letter ind
R691:691 untypedLC <> letter ind
R698:698 untypedLC <> letter ind
R705:705 untypedLC <> letter ind
R712:712 untypedLC <> letter ind
R719:719 untypedLC <> letter ind
R726:726 untypedLC <> letter ind
R733:733 untypedLC <> letter ind
R740:740 untypedLC <> letter ind
R747:747 untypedLC <> letter ind
R754:754 untypedLC <> letter ind
R761:761 untypedLC <> letter ind
R768:768 untypedLC <> letter ind
R775:775 untypedLC <> letter ind
R782:782 untypedLC <> letter ind
R789:789 untypedLC <> letter ind
R796:796 untypedLC <> letter ind
R803:803 untypedLC <> letter ind
R810:810 untypedLC <> letter ind
R817:817 untypedLC <> letter ind
R824:824 untypedLC <> letter ind
R831:831 untypedLC <> letter ind
R838:838 untypedLC <> letter ind
R845:845 untypedLC <> letter ind
R852:852 untypedLC <> letter ind
R859:859 untypedLC <> letter ind
R866:866 untypedLC <> letter ind
def 881:893 <> nat_of_letter
R908:908 untypedLC <> x var
R919:919 untypedLC <> a constr
R931:931 untypedLC <> b constr
R943:943 untypedLC <> c constr
R955:955 untypedLC <> d constr
R967:967 untypedLC <> e constr
R979:979 untypedLC <> f constr
R992:992 untypedLC <> g constr
R1004:1004 untypedLC <> h constr
R1016:1016 untypedLC <> i constr
R1028:1028 untypedLC <> j constr
R1040:1040 untypedLC <> k constr
R1052:1052 untypedLC <> l constr
R1065:1065 untypedLC <> m constr
R1077:1077 untypedLC <> n constr
R1089:1089 untypedLC <> o constr
R1101:1101 untypedLC <> p constr
R1113:1113 untypedLC <> q constr
R1125:1125 untypedLC <> r constr
R1138:1138 untypedLC <> s constr
R1150:1150 untypedLC <> t constr
R1162:1162 untypedLC <> u constr
R1174:1174 untypedLC <> v constr
R1186:1186 untypedLC <> w constr
R1198:1198 untypedLC <> x constr
R1211:1211 untypedLC <> y constr
R1223:1223 untypedLC <> z constr
R1236:1237 untypedLC <> a1 constr
R1248:1249 untypedLC <> b1 constr
R1260:1261 untypedLC <> c1 constr
R1272:1273 untypedLC <> d1 constr
R1284:1285 untypedLC <> e1 constr
R1296:1297 untypedLC <> f1 constr
R1309:1310 untypedLC <> g1 constr
R1321:1322 untypedLC <> h1 constr
R1333:1334 untypedLC <> i1 constr
R1345:1346 untypedLC <> j1 constr
R1357:1358 untypedLC <> k1 constr
R1369:1370 untypedLC <> l1 constr
R1382:1383 untypedLC <> m1 constr
R1394:1395 untypedLC <> n1 constr
R1406:1407 untypedLC <> o1 constr
R1418:1419 untypedLC <> p1 constr
R1430:1431 untypedLC <> q1 constr
R1442:1443 untypedLC <> r1 constr
R1455:1456 untypedLC <> s1 constr
R1467:1468 untypedLC <> t1 constr
R1479:1480 untypedLC <> u1 constr
R1491:1492 untypedLC <> v1 constr
R1503:1504 untypedLC <> w1 constr
R1515:1516 untypedLC <> x1 constr
R1528:1529 untypedLC <> y1 constr
R1540:1541 untypedLC <> z1 constr
def 1568:1580 <> letter_of_nat
R1596:1597 untypedLC <> nn var
R1615:1615 untypedLC <> a constr
R1627:1627 untypedLC <> b constr
R1639:1639 untypedLC <> c constr
R1651:1651 untypedLC <> d constr
R1663:1663 untypedLC <> e constr
R1675:1675 untypedLC <> f constr
R1688:1688 untypedLC <> g constr
R1700:1700 untypedLC <> h constr
R1712:1712 untypedLC <> i constr
R1724:1724 untypedLC <> j constr
R1736:1736 untypedLC <> k constr
R1748:1748 untypedLC <> l constr
R1761:1761 untypedLC <> m constr
R1773:1773 untypedLC <> n constr
R1785:1785 untypedLC <> o constr
R1797:1797 untypedLC <> p constr
R1809:1809 untypedLC <> q constr
R1821:1821 untypedLC <> r constr
R1834:1834 untypedLC <> s constr
R1846:1846 untypedLC <> t constr
R1858:1858 untypedLC <> u constr
R1870:1870 untypedLC <> v constr
R1882:1882 untypedLC <> w constr
R1894:1894 untypedLC <> x constr
R1907:1907 untypedLC <> y constr
R1919:1919 untypedLC <> z constr
R1931:1932 untypedLC <> a1 constr
R1943:1944 untypedLC <> b1 constr
R1955:1956 untypedLC <> c1 constr
R1967:1968 untypedLC <> d1 constr
R1979:1980 untypedLC <> e1 constr
R1991:1992 untypedLC <> f1 constr
R2004:2005 untypedLC <> g1 constr
R2016:2017 untypedLC <> h1 constr
R2028:2029 untypedLC <> i1 constr
R2040:2041 untypedLC <> j1 constr
R2052:2053 untypedLC <> k1 constr
R2064:2065 untypedLC <> l1 constr
R2077:2078 untypedLC <> m1 constr
R2089:2090 untypedLC <> n1 constr
R2101:2102 untypedLC <> o1 constr
R2113:2114 untypedLC <> p1 constr
R2125:2126 untypedLC <> q1 constr
R2137:2138 untypedLC <> r1 constr
R2150:2151 untypedLC <> s1 constr
R2162:2163 untypedLC <> t1 constr
R2174:2175 untypedLC <> u1 constr
R2186:2187 untypedLC <> v1 constr
R2198:2199 untypedLC <> w1 constr
R2210:2211 untypedLC <> x1 constr
R2223:2224 untypedLC <> y1 constr
R2235:2236 untypedLC <> z1 constr
R2247:2247 untypedLC <> a constr
def 2279:2290 <> first_letter
R2295:2295 untypedLC <> a constr
def 2309:2319 <> card_letter
ind 2346:2349 <> Name
constr 2362:2365 <> Lett
constr 2386:2390 <> Prime
R2375:2378 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2379:2382 untypedLC <> Name ind
R2369:2374 untypedLC <> letter ind
R2398:2401 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2402:2405 untypedLC <> Name ind
R2394:2397 untypedLC <> Name ind
R2410:2439 untypedLC <> Lett constr
R2463:2467 untypedLC <> Prime constr
not 2452:2452 <> :::x_'°'
def 2511:2521 <> nat_of_Name
R2537:2538 untypedLC <> nn var
R2549:2552 untypedLC <> Lett constr
R2560:2572 untypedLC <> nat_of_letter def
R2581:2585 untypedLC <> Prime constr
R2604:2606 Coq.Init.Peano <> ::nat_scope:x_'+'_x not
R2593:2603 untypedLC <> card_letter def
R2607:2617 untypedLC <> nat_of_Name def
R2619:2620 untypedLC <> nn var
def 2641:2648 <> eqb_Name
R2658:2661 Coq.Init.Datatypes <> bool ind
R2666:2668 Coq.Init.Nat <> eqb def
R2688:2698 untypedLC <> nat_of_Name def
R2700:2701 untypedLC <> ay var
R2671:2681 untypedLC <> nat_of_Name def
R2683:2684 untypedLC <> ax var
def 2736:2742 <> rot_nat
R2756:2758 Coq.Init.Nat <> eqb def
R2766:2776 untypedLC <> card_letter def
R2761:2761 Coq.Init.Datatypes <> S constr
R2763:2763 untypedLC <> n var
R2790:2790 Coq.Init.Datatypes <> S constr
R2792:2792 untypedLC <> n var
R2783:2783 Coq.Init.Datatypes <> O constr
def 2807:2816 <> rot_letter
R2823:2835 untypedLC <> letter_of_nat def
R2838:2844 untypedLC <> rot_nat def
R2847:2859 untypedLC <> nat_of_letter def
R2861:2861 untypedLC <> x var
def 2876:2884 <> next_name
R2900:2901 untypedLC <> nn var
R2912:2915 untypedLC <> Lett constr
R2937:2943 untypedLC <> rot_nat def
R2946:2958 untypedLC <> nat_of_letter def
R2977:2978 untypedLC <> rn var
R2991:2991 Coq.Init.Datatypes <> O constr
R2996:3000 untypedLC <> Prime constr
R3002:3013 untypedLC <> first_letter def
R3026:3029 untypedLC <> Lett constr
R3032:3044 untypedLC <> letter_of_nat def
R3046:3047 untypedLC <> rn var
R3062:3066 untypedLC <> Prime constr
R3074:3078 untypedLC <> Prime constr
R3081:3089 untypedLC <> next_name def
R3091:3092 untypedLC <> nn var
def 3112:3120 <> gen_names
R3138:3141 Coq.Init.Datatypes <> list ind
R3143:3143 untypedLC <> A var
R3150:3153 Coq.Init.Datatypes <> list ind
R3155:3158 untypedLC <> Name ind
R3171:3172 untypedLC <> ll var
R3183:3184 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R3189:3189 Coq.Lists.List ListNotations ::list_scope:'['_x_']' not
R3191:3191 Coq.Lists.List ListNotations ::list_scope:'['_x_']' not
R3190:3190 untypedLC <> n var
R3198:3201 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3209:3212 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3208:3208 untypedLC <> n var
R3213:3221 untypedLC <> gen_names def
R3227:3235 untypedLC <> next_name def
R3237:3237 untypedLC <> n var
R3223:3224 untypedLC <> ll var
def 3314:3319 <> mayrem
R3325:3328 untypedLC <> Name ind
R3335:3338 Coq.Init.Datatypes <> list ind
R3340:3343 untypedLC <> Name ind
R3348:3353 Coq.Init.Datatypes <> option ind
R3356:3359 Coq.Init.Datatypes <> list ind
R3361:3364 untypedLC <> Name ind
R3378:3379 untypedLC <> ll var
R3390:3391 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R3396:3399 Coq.Init.Datatypes <> None constr
R3408:3411 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3429:3434 untypedLC <> mayrem def
R3436:3437 untypedLC <> ax var
R3454:3457 Coq.Init.Datatypes <> None constr
R3465:3472 untypedLC <> eqb_Name def
R3474:3475 untypedLC <> ax var
R3500:3503 Coq.Init.Datatypes <> None constr
R3486:3489 Coq.Init.Datatypes <> Some constr
R3511:3514 Coq.Init.Datatypes <> Some constr
R3527:3534 untypedLC <> eqb_Name def
R3536:3537 untypedLC <> ax var
R3563:3566 Coq.Init.Datatypes <> Some constr
R3572:3575 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3548:3551 Coq.Init.Datatypes <> Some constr
def 3730:3736 <> fresh_1
R3744:3747 untypedLC <> Name ind
R3767:3770 Coq.Init.Datatypes <> list ind
R3772:3775 untypedLC <> Name ind
R3780:3783 untypedLC <> Name ind
R3796:3802 untypedLC <> lstruct var
R3813:3814 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R3819:3822 untypedLC <> cand var
R3829:3832 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R3851:3856 untypedLC <> mayrem def
R3863:3868 untypedLC <> lavoid var
R3858:3861 untypedLC <> cand var
R3898:3901 Coq.Init.Datatypes <> None constr
R3906:3909 untypedLC <> cand var
R3934:3937 Coq.Init.Datatypes <> Some constr
R3950:3956 untypedLC <> fresh_1 def
R3959:3967 untypedLC <> next_name def
R3969:3972 untypedLC <> cand var
def 4036:4040 <> fresh
R4049:4052 Coq.Init.Datatypes <> list ind
R4054:4057 untypedLC <> Name ind
R4062:4065 untypedLC <> Name ind
R4070:4076 untypedLC <> fresh_1 def
R4097:4101 untypedLC <> avoid var
R4091:4095 untypedLC <> avoid var
R4078:4089 untypedLC <> first_letter def
ind 4219:4222 <> lexp
constr 4238:4240 <> Var
constr 4261:4263 <> Lam
constr 4292:4294 <> App
R4248:4251 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4252:4255 untypedLC <> lexp ind
R4244:4247 untypedLC <> Name ind
R4271:4274 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4279:4282 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4283:4286 untypedLC <> lexp ind
R4275:4278 untypedLC <> lexp ind
R4267:4270 untypedLC <> Name ind
R4302:4305 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4310:4313 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R4314:4317 untypedLC <> lexp ind
R4306:4309 untypedLC <> lexp ind
R4298:4301 untypedLC <> lexp ind
R4400:4402 untypedLC <> Lam constr
R4410:4412 untypedLC <> Lam constr
not 4381:4381 <> :::'\'_x_'..'_x_'~'_x
R4519:4521 untypedLC <> Lam constr
R4529:4531 untypedLC <> Lam constr
not 4499:4499 <> :::'\'_x_'..'_x_'·'_x
R4641:4643 untypedLC <> Lam constr
R4651:4653 untypedLC <> Lam constr
not 4618:4618 <> :::'λ'_x_'..'_x_'·'_x
R4732:4758 untypedLC <> Var constr
R4762:4792 untypedLC <> App constr
def 5100:5102 <> mem
R5108:5111 untypedLC <> Name ind
R5118:5121 Coq.Init.Datatypes <> list ind
R5123:5126 untypedLC <> Name ind
R5131:5134 Coq.Init.Datatypes <> bool ind
R5147:5148 untypedLC <> xx var
R5159:5160 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5165:5169 Coq.Init.Datatypes <> false constr
R5178:5181 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5192:5199 untypedLC <> eqb_Name def
R5201:5202 untypedLC <> ax var
R5223:5225 untypedLC <> mem def
R5227:5228 untypedLC <> ax var
R5213:5216 Coq.Init.Datatypes <> true constr
def 5291:5293 <> rem
R5299:5302 untypedLC <> Name ind
R5309:5312 Coq.Init.Datatypes <> list ind
R5314:5317 untypedLC <> Name ind
R5322:5325 Coq.Init.Datatypes <> list ind
R5327:5330 untypedLC <> Name ind
R5343:5344 untypedLC <> xx var
R5355:5356 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5361:5362 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5371:5374 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5385:5392 untypedLC <> eqb_Name def
R5394:5395 untypedLC <> ax var
R5443:5446 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5447:5449 untypedLC <> rem def
R5451:5452 untypedLC <> ax var
R5406:5408 untypedLC <> rem def
R5410:5411 untypedLC <> ax var
def 5519:5526 <> make_set
R5533:5536 Coq.Init.Datatypes <> list ind
R5538:5541 untypedLC <> Name ind
R5554:5555 untypedLC <> xx var
R5566:5567 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5572:5573 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5581:5584 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5595:5597 untypedLC <> mem def
R5648:5652 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5665:5665 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5653:5660 untypedLC <> make_set def
R5611:5618 untypedLC <> make_set def
def 5725:5731 <> inter_1
R5741:5744 Coq.Init.Datatypes <> list ind
R5746:5749 untypedLC <> Name ind
R5762:5763 untypedLC <> xx var
R5774:5775 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5780:5781 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R5789:5792 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5803:5805 untypedLC <> mem def
R5810:5811 untypedLC <> yx var
R5861:5867 untypedLC <> inter_1 def
R5873:5874 untypedLC <> yx var
R5820:5823 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R5824:5830 untypedLC <> inter_1 def
R5836:5837 untypedLC <> yx var
def 5895:5899 <> inter
R5909:5912 Coq.Init.Datatypes <> list ind
R5914:5917 untypedLC <> Name ind
R5922:5928 untypedLC <> inter_1 def
R5944:5945 untypedLC <> yx var
R5931:5938 untypedLC <> make_set def
R5940:5941 untypedLC <> xx var
def 5998:6004 <> allvars
R6011:6014 Coq.Init.Datatypes <> list ind
R6016:6019 untypedLC <> Name ind
R6032:6033 untypedLC <> ex var
R6044:6046 untypedLC <> Var constr
R6054:6054 Coq.Lists.List ListNotations ::list_scope:'['_x_']' not
R6057:6057 Coq.Lists.List ListNotations ::list_scope:'['_x_']' not
R6063:6065 untypedLC <> Lam constr
R6078:6082 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6093:6093 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6083:6089 untypedLC <> allvars def
R6091:6092 untypedLC <> ex var
R6099:6101 untypedLC <> App constr
R6125:6128 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R6114:6120 untypedLC <> allvars def
R6129:6135 untypedLC <> allvars def
def 6160:6163 <> vars
R6171:6178 untypedLC <> make_set def
R6181:6187 untypedLC <> allvars def
R6189:6190 untypedLC <> ex var
def 6266:6273 <> freevars
R6280:6283 Coq.Init.Datatypes <> list ind
R6285:6288 untypedLC <> Name ind
R6301:6302 untypedLC <> ex var
R6313:6315 untypedLC <> Var constr
R6323:6323 Coq.Lists.List ListNotations ::list_scope:'['_x_']' not
R6326:6326 Coq.Lists.List ListNotations ::list_scope:'['_x_']' not
R6332:6334 untypedLC <> Lam constr
R6345:6347 untypedLC <> rem def
R6353:6360 untypedLC <> freevars def
R6362:6363 untypedLC <> ex var
R6370:6372 untypedLC <> App constr
R6397:6400 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R6385:6392 untypedLC <> freevars def
R6401:6408 untypedLC <> freevars def
def 6433:6439 <> vlibres
R6447:6454 untypedLC <> make_set def
R6457:6464 untypedLC <> freevars def
R6466:6467 untypedLC <> ex var
def 6544:6552 <> boundvars
R6559:6562 Coq.Init.Datatypes <> list ind
R6564:6567 untypedLC <> Name ind
R6580:6581 untypedLC <> ex var
R6592:6594 untypedLC <> Var constr
R6602:6603 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R6609:6611 untypedLC <> Lam constr
R6625:6627 untypedLC <> mem def
R6633:6640 untypedLC <> freevars def
R6642:6643 untypedLC <> ex var
R6694:6702 untypedLC <> boundvars def
R6704:6705 untypedLC <> ex var
R6653:6657 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6670:6670 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6658:6666 untypedLC <> boundvars def
R6668:6669 untypedLC <> ex var
R6711:6713 untypedLC <> App constr
R6739:6742 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R6726:6734 untypedLC <> boundvars def
R6743:6751 untypedLC <> boundvars def
def 6776:6781 <> vliees
R6789:6796 untypedLC <> make_set def
R6799:6807 untypedLC <> boundvars def
R6809:6810 untypedLC <> ex var
def 6824:6835 <> declaredvars
R6842:6845 Coq.Init.Datatypes <> list ind
R6847:6850 untypedLC <> Name ind
R6863:6864 untypedLC <> ex var
R6875:6877 untypedLC <> Var constr
R6885:6886 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R6892:6894 untypedLC <> Lam constr
R6907:6911 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6927:6927 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R6912:6923 untypedLC <> declaredvars def
R6925:6926 untypedLC <> ex var
R6933:6935 untypedLC <> App constr
R6964:6967 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R6948:6959 untypedLC <> declaredvars def
R6968:6979 untypedLC <> declaredvars def
def 7004:7007 <> vdef
R7015:7022 untypedLC <> make_set def
R7025:7036 untypedLC <> declaredvars def
R7038:7039 untypedLC <> ex var
def 7185:7190 <> rename
R7202:7205 untypedLC <> lexp ind
R7218:7219 untypedLC <> ex var
R7230:7232 untypedLC <> Var constr
R7248:7255 untypedLC <> eqb_Name def
R7260:7261 untypedLC <> ny var
R7280:7281 untypedLC <> ex var
R7268:7270 untypedLC <> Var constr
R7272:7273 untypedLC <> nz var
R7287:7289 untypedLC <> Lam constr
R7305:7312 untypedLC <> eqb_Name def
R7317:7318 untypedLC <> ny var
R7354:7356 untypedLC <> Lam constr
R7362:7367 untypedLC <> rename def
R7372:7373 untypedLC <> nz var
R7369:7370 untypedLC <> ny var
R7325:7326 untypedLC <> ex var
R7384:7386 untypedLC <> App constr
R7399:7401 untypedLC <> App constr
R7423:7428 untypedLC <> rename def
R7433:7434 untypedLC <> nz var
R7430:7431 untypedLC <> ny var
R7404:7409 untypedLC <> rename def
R7414:7415 untypedLC <> nz var
R7411:7412 untypedLC <> ny var
def 7590:7594 <> alpha
R7606:7609 untypedLC <> lexp ind
R7622:7623 untypedLC <> ex var
R7634:7636 untypedLC <> Var constr
R7649:7651 untypedLC <> Var constr
R7660:7662 untypedLC <> Lam constr
R7686:7690 untypedLC <> alpha def
R7695:7696 untypedLC <> nz var
R7692:7693 untypedLC <> ny var
R7727:7734 untypedLC <> eqb_Name def
R7739:7740 untypedLC <> ny var
R7797:7799 untypedLC <> Lam constr
R7804:7806 untypedLC <> ex2 var
R7747:7749 untypedLC <> Lam constr
R7755:7760 untypedLC <> rename def
R7768:7770 untypedLC <> ex2 var
R7765:7766 untypedLC <> nz var
R7751:7752 untypedLC <> nz var
R7812:7814 untypedLC <> App constr
R7827:7829 untypedLC <> App constr
R7850:7854 untypedLC <> alpha def
R7859:7860 untypedLC <> nz var
R7856:7857 untypedLC <> ny var
R7832:7836 untypedLC <> alpha def
R7841:7842 untypedLC <> nz var
R7838:7839 untypedLC <> ny var
def 8159:8166 <> renaming
R8191:8192 untypedLC <> fv var
R8203:8204 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R8209:8210 untypedLC <> ex var
R8218:8221 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R8250:8254 untypedLC <> fresh def
R8256:8260 untypedLC <> avoid var
R8269:8276 untypedLC <> renaming def
R8304:8308 untypedLC <> alpha def
R8323:8324 untypedLC <> ex var
R8313:8321 untypedLC <> freshname var
R8292:8295 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R8283:8291 untypedLC <> freshname var
R8296:8300 untypedLC <> avoid var
def 8392:8398 <> subst_1
R8412:8415 untypedLC <> lexp ind
R8428:8430 untypedLC <> ex1 var
R8441:8443 untypedLC <> Var constr
R8461:8468 untypedLC <> eqb_Name def
R8473:8474 untypedLC <> nz var
R8490:8492 untypedLC <> ex1 var
R8481:8483 untypedLC <> ex2 var
R8498:8500 untypedLC <> Lam constr
R8518:8525 untypedLC <> eqb_Name def
R8530:8531 untypedLC <> nz var
R8568:8570 untypedLC <> Lam constr
R8576:8582 untypedLC <> subst_1 def
R8587:8589 untypedLC <> ex2 var
R8584:8585 untypedLC <> nz var
R8538:8540 untypedLC <> ex1 var
R8599:8601 untypedLC <> App constr
R8616:8618 untypedLC <> App constr
R8643:8649 untypedLC <> subst_1 def
R8654:8656 untypedLC <> ex2 var
R8651:8652 untypedLC <> nz var
R8621:8627 untypedLC <> subst_1 def
R8632:8634 untypedLC <> ex2 var
R8629:8630 untypedLC <> nz var
def 8754:8758 <> subst
R8773:8776 untypedLC <> lexp ind
R8793:8797 untypedLC <> inter def
R8811:8817 untypedLC <> vlibres def
R8819:8821 untypedLC <> ex2 var
R8800:8803 untypedLC <> vdef def
R8805:8807 untypedLC <> ex1 var
R8842:8848 untypedLC <> allvars def
R8850:8852 untypedLC <> ex1 var
R8859:8865 untypedLC <> subst_1 def
R8875:8882 untypedLC <> renaming def
R8893:8895 untypedLC <> ex1 var
R8887:8891 untypedLC <> avoid var
R8884:8885 untypedLC <> vx var
R8870:8872 untypedLC <> ex2 var
R8867:8868 untypedLC <> nx var
def 9027:9033 <> redexes
R9041:9044 Coq.Init.Datatypes <> list ind
R9046:9049 untypedLC <> lexp ind
R9062:9063 untypedLC <> ex var
R9074:9076 untypedLC <> Var constr
R9096:9097 Coq.Lists.List ListNotations ::list_scope:'['_']' not
R9103:9105 untypedLC <> App constr
R9108:9110 untypedLC <> Lam constr
R9125:9125 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R9144:9149 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R9174:9174 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R9126:9128 untypedLC <> App constr
R9131:9133 untypedLC <> Lam constr
R9160:9163 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R9150:9156 untypedLC <> redexes def
R9164:9170 untypedLC <> redexes def
R9180:9182 untypedLC <> App constr
R9212:9215 Coq.Init.Datatypes <> ::list_scope:x_'++'_x not
R9202:9208 untypedLC <> redexes def
R9216:9222 untypedLC <> redexes def
R9231:9233 untypedLC <> Lam constr
R9253:9259 untypedLC <> redexes def
ind 9300:9302 <> occ
constr 9315:9317 <> Ici
constr 9321:9322 <> UL
constr 9354:9355 <> LA
constr 9390:9391 <> RA
R9318:9318 untypedLC <> occ ind
R9329:9332 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9333:9335 untypedLC <> occ ind
R9326:9328 untypedLC <> occ ind
R9362:9365 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9366:9368 untypedLC <> occ ind
R9359:9361 untypedLC <> occ ind
R9398:9401 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9402:9404 untypedLC <> occ ind
R9395:9397 untypedLC <> occ ind
def 9443:9447 <> no_UL
R9454:9457 Coq.Init.Datatypes <> bool ind
R9470:9471 untypedLC <> oc var
R9482:9484 untypedLC <> Ici constr
R9489:9492 Coq.Init.Datatypes <> true constr
R9498:9499 untypedLC <> UL constr
R9506:9510 Coq.Init.Datatypes <> false constr
R9516:9517 untypedLC <> LA constr
R9525:9529 untypedLC <> no_UL def
R9531:9532 untypedLC <> oc var
R9538:9539 untypedLC <> RA constr
R9547:9551 untypedLC <> no_UL def
R9553:9554 untypedLC <> oc var
def 9615:9622 <> smtg_occ
R9686:9687 untypedLC <> ex var
R9682:9683 untypedLC <> oc var
R9701:9703 untypedLC <> Ici constr
R9711:9713 untypedLC <> chk var
R9715:9716 untypedLC <> ex var
R9725:9726 untypedLC <> UL constr
R9732:9734 untypedLC <> Lam constr
R9744:9746 untypedLC <> aux var
R9748:9749 untypedLC <> oc var
R9761:9762 untypedLC <> LA constr
R9768:9770 untypedLC <> App constr
R9781:9783 untypedLC <> aux var
R9785:9786 untypedLC <> oc var
R9798:9799 untypedLC <> RA constr
R9805:9807 untypedLC <> App constr
R9818:9820 untypedLC <> aux var
R9822:9823 untypedLC <> oc var
R9843:9847 Coq.Init.Logic <> False ind
R9862:9863 untypedLC <> ex var
R9859:9860 untypedLC <> oc var
def 9878:9884 <> anyterm
R9892:9895 untypedLC <> lexp ind
R9901:9904 Coq.Init.Logic <> True ind
def 9938:9940 <> rar
R9948:9951 untypedLC <> lexp ind
R9965:9966 untypedLC <> ex var
R9977:9979 untypedLC <> App constr
R9982:9984 untypedLC <> :::'λ'_x_'..'_x_'·'_x not
R9986:9989 untypedLC <> :::'λ'_x_'..'_x_'·'_x not
R9998:10001 Coq.Init.Logic <> True ind
R10012:10016 Coq.Init.Logic <> False ind
def 10059:10061 <> fvr
R10068:10071 untypedLC <> Name ind
R10080:10083 untypedLC <> lexp ind
R10097:10098 untypedLC <> ex var
R10109:10111 untypedLC <> Var constr
R10122:10129 untypedLC <> eqb_Name def
R10131:10132 untypedLC <> nx var
R10152:10156 Coq.Init.Logic <> False ind
R10142:10145 Coq.Init.Logic <> True ind
R10167:10171 Coq.Init.Logic <> False ind
def 10192:10198 <> has_occ
R10203:10210 untypedLC <> smtg_occ def
R10212:10218 untypedLC <> anyterm def
def 10232:10238 <> has_red
R10243:10250 untypedLC <> smtg_occ def
R10252:10254 untypedLC <> rar def
prf 10264:10276 <> has_occ_UL_LA
R10312:10315 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10335:10338 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10339:10343 Coq.Init.Logic <> False ind
R10316:10322 untypedLC <> has_occ def
R10333:10334 untypedLC <> ex var
R10325:10326 untypedLC <> LA constr
R10328:10330 untypedLC <> oc2 var
R10293:10299 untypedLC <> has_occ def
R10310:10311 untypedLC <> ex var
R10302:10303 untypedLC <> UL constr
R10305:10307 untypedLC <> oc1 var
prf 10398:10410 <> has_occ_UL_RA
R10446:10449 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10469:10472 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10473:10477 Coq.Init.Logic <> False ind
R10450:10456 untypedLC <> has_occ def
R10467:10468 untypedLC <> ex var
R10459:10460 untypedLC <> RA constr
R10462:10464 untypedLC <> oc2 var
R10427:10433 untypedLC <> has_occ def
R10444:10445 untypedLC <> ex var
R10436:10437 untypedLC <> UL constr
R10439:10441 untypedLC <> oc1 var
def 10535:10544 <> subterm_at
R10567:10570 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10571:10574 untypedLC <> lexp ind
R10554:10560 untypedLC <> has_occ def
R10565:10566 untypedLC <> ex var
R10562:10563 untypedLC <> oc var
R10594:10595 untypedLC <> ex var
R10590:10591 untypedLC <> oc var
R10617:10620 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10621:10624 untypedLC <> lexp ind
R10604:10610 untypedLC <> has_occ def
R10615:10616 untypedLC <> ex var
R10612:10613 untypedLC <> oc var
R10638:10640 untypedLC <> Ici constr
R10659:10660 untypedLC <> ex var
R10669:10670 untypedLC <> UL constr
R10676:10678 untypedLC <> Lam constr
R10699:10708 untypedLC <> subterm_at def
R10716:10718 untypedLC <> oec var
R10713:10714 untypedLC <> oc var
R10727:10728 untypedLC <> LA constr
R10734:10736 untypedLC <> App constr
R10758:10767 untypedLC <> subterm_at def
R10775:10777 untypedLC <> oec var
R10772:10773 untypedLC <> oc var
R10786:10787 untypedLC <> RA constr
R10793:10795 untypedLC <> App constr
R10817:10826 untypedLC <> subterm_at def
R10834:10836 untypedLC <> oec var
R10831:10832 untypedLC <> oc var
R10870:10872 untypedLC <> oec var
def 10905:10914 <> rewrite_at
R10927:10930 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10923:10926 untypedLC <> lexp ind
R10961:10964 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10965:10968 untypedLC <> lexp ind
R10955:10957 untypedLC <> chk var
R10959:10960 untypedLC <> ex var
R11006:11013 untypedLC <> smtg_occ def
R11022:11023 untypedLC <> ex var
R11019:11020 untypedLC <> oc var
R11015:11017 untypedLC <> chk var
R11028:11031 untypedLC <> lexp ind
R11075:11078 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R11079:11082 untypedLC <> lexp ind
R11057:11064 untypedLC <> smtg_occ def
R11073:11074 untypedLC <> ex var
R11070:11071 untypedLC <> oc var
R11066:11068 untypedLC <> chk var
R11102:11103 untypedLC <> ex var
R11098:11099 untypedLC <> oc var
R11130:11133 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R11134:11137 untypedLC <> lexp ind
R11112:11119 untypedLC <> smtg_occ def
R11128:11129 untypedLC <> ex var
R11125:11126 untypedLC <> oc var
R11121:11123 untypedLC <> chk var
R11151:11153 untypedLC <> Ici constr
R11172:11175 untypedLC <> rewf var
R11180:11182 untypedLC <> oec var
R11177:11178 untypedLC <> ex var
R11191:11192 untypedLC <> UL constr
R11198:11200 untypedLC <> Lam constr
R11222:11224 untypedLC <> Lam constr
R11230:11235 untypedLC <> rew_at var
R11243:11245 untypedLC <> oec var
R11240:11241 untypedLC <> oc var
R11255:11256 untypedLC <> LA constr
R11262:11264 untypedLC <> App constr
R11286:11288 untypedLC <> App constr
R11291:11296 untypedLC <> rew_at var
R11304:11306 untypedLC <> oec var
R11301:11302 untypedLC <> oc var
R11319:11320 untypedLC <> RA constr
R11326:11328 untypedLC <> App constr
R11350:11352 untypedLC <> App constr
R11358:11363 untypedLC <> rew_at var
R11371:11373 untypedLC <> oec var
R11368:11369 untypedLC <> oc var
R11408:11410 untypedLC <> oec var
R11437:11439 untypedLC <> oec var
R11434:11435 untypedLC <> oc var
R11431:11432 untypedLC <> ex var
ind 11957:11963 <> gocc_of
constr 12000:12002 <> o_o
R11976:11979 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R11972:11975 untypedLC <> lexp ind
R12035:12038 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12039:12045 untypedLC <> gocc_of ind
R12051:12052 untypedLC <> ex var
R12047:12049 untypedLC <> chk var
R12017:12024 untypedLC <> smtg_occ def
R12033:12034 untypedLC <> ex var
R12030:12031 untypedLC <> oc var
R12026:12028 untypedLC <> chk var
def 12066:12071 <> occ_of
R12076:12082 untypedLC <> gocc_of ind
R12084:12090 untypedLC <> anyterm def
def 12104:12110 <> rocc_of
R12115:12121 untypedLC <> gocc_of ind
R12123:12125 untypedLC <> rar def
def 12139:12147 <> lift_test
R12156:12159 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12160:12163 Coq.Init.Datatypes <> bool ind
R12153:12155 untypedLC <> occ ind
R12179:12185 untypedLC <> gocc_of ind
R12191:12192 untypedLC <> ex var
R12187:12189 untypedLC <> chk var
R12197:12200 Coq.Init.Datatypes <> bool ind
R12222:12223 untypedLC <> go var
R12228:12228 untypedLC <> f var
R12230:12231 untypedLC <> oc var
prf 12247:12259 <> smtg_occ_impl
R12278:12281 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12274:12277 untypedLC <> lexp ind
R12292:12292 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12322:12326 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12360:12363 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12364:12371 untypedLC <> smtg_occ def
R12381:12382 untypedLC <> ex var
R12378:12379 untypedLC <> oc var
R12373:12376 untypedLC <> chk2 var
R12341:12348 untypedLC <> smtg_occ def
R12358:12359 untypedLC <> ex var
R12355:12356 untypedLC <> oc var
R12350:12353 untypedLC <> chk1 var
R12311:12314 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12315:12318 untypedLC <> chk2 var
R12320:12321 untypedLC <> ex var
R12304:12307 untypedLC <> chk1 var
R12309:12310 untypedLC <> ex var
R12455:12456 untypedLC <> ex var
R12451:12452 untypedLC <> oc var
R12470:12472 untypedLC <> Ici constr
R12485:12486 untypedLC <> ex var
R12495:12496 untypedLC <> UL constr
R12502:12504 untypedLC <> Lam constr
R12514:12516 untypedLC <> aux var
R12518:12519 untypedLC <> oc var
R12531:12532 untypedLC <> LA constr
R12538:12540 untypedLC <> App constr
R12551:12553 untypedLC <> aux var
R12555:12556 untypedLC <> oc var
R12568:12569 untypedLC <> RA constr
R12575:12577 untypedLC <> App constr
R12588:12590 untypedLC <> aux var
R12592:12593 untypedLC <> oc var
R12622:12622 untypedLC <> F var
R12455:12456 untypedLC <> ex var
R12451:12452 untypedLC <> oc var
R12470:12472 untypedLC <> Ici constr
R12485:12486 untypedLC <> ex var
R12495:12496 untypedLC <> UL constr
R12502:12504 untypedLC <> Lam constr
R12514:12516 untypedLC <> aux var
R12518:12519 untypedLC <> oc var
R12531:12532 untypedLC <> LA constr
R12538:12540 untypedLC <> App constr
R12551:12553 untypedLC <> aux var
R12555:12556 untypedLC <> oc var
R12568:12569 untypedLC <> RA constr
R12575:12577 untypedLC <> App constr
R12588:12590 untypedLC <> aux var
R12592:12593 untypedLC <> oc var
R12622:12622 untypedLC <> F var
prf 12662:12670 <> gocc_impl
R12689:12692 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12685:12688 untypedLC <> lexp ind
R12703:12703 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12733:12737 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12764:12767 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12768:12774 untypedLC <> gocc_of ind
R12781:12782 untypedLC <> ex var
R12776:12779 untypedLC <> chk2 var
R12749:12755 untypedLC <> gocc_of ind
R12762:12763 untypedLC <> ex var
R12757:12760 untypedLC <> chk1 var
R12722:12725 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12726:12729 untypedLC <> chk2 var
R12731:12732 untypedLC <> ex var
R12715:12718 untypedLC <> chk1 var
R12720:12721 untypedLC <> ex var
R12837:12849 untypedLC <> smtg_occ_impl thm
R12837:12849 untypedLC <> smtg_occ_impl thm
prf 12886:12893 <> rocc_occ
R12912:12915 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R12916:12921 untypedLC <> occ_of def
R12923:12924 untypedLC <> ex var
R12902:12908 untypedLC <> rocc_of def
R12910:12911 untypedLC <> ex var
R12943:12951 untypedLC <> gocc_impl thm
R12957:12963 untypedLC <> anyterm def
R12953:12955 untypedLC <> rar def
R12943:12951 untypedLC <> gocc_impl thm
R12957:12963 untypedLC <> anyterm def
R12953:12955 untypedLC <> rar def
R12998:12998 Coq.Init.Logic <> I constr
R12998:12998 Coq.Init.Logic <> I constr
def 13056:13067 <> subterm_at_g
R13078:13083 untypedLC <> occ_of def
R13085:13086 untypedLC <> ex var
R13091:13094 untypedLC <> lexp ind
R13118:13119 untypedLC <> oe var
R13124:13133 untypedLC <> subterm_at def
R13141:13143 untypedLC <> oec var
R13138:13139 untypedLC <> oc var
R13135:13136 untypedLC <> ex var
def 13157:13169 <> subterm_at_gr
R13180:13186 untypedLC <> rocc_of def
R13188:13189 untypedLC <> ex var
R13194:13197 untypedLC <> lexp ind
R13204:13215 untypedLC <> subterm_at_g def
R13221:13228 untypedLC <> rocc_occ thm
R13230:13231 untypedLC <> oe var
R13217:13218 untypedLC <> ex var
def 13247:13258 <> rewrite_at_g
R13278:13284 untypedLC <> gocc_of ind
R13290:13291 untypedLC <> ex var
R13286:13288 untypedLC <> chk var
R13296:13299 untypedLC <> lexp ind
R13323:13324 untypedLC <> oe var
R13329:13338 untypedLC <> rewrite_at def
R13355:13357 untypedLC <> oec var
R13352:13353 untypedLC <> oc var
R13349:13350 untypedLC <> ex var
R13344:13347 untypedLC <> rewf var
R13340:13342 untypedLC <> chk var
def 13372:13381 <> root_subst
R13394:13397 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R13398:13401 untypedLC <> lexp ind
R13388:13390 untypedLC <> rar def
R13392:13393 untypedLC <> ex var
R13414:13415 untypedLC <> ex var
R13426:13428 untypedLC <> App constr
R13431:13433 untypedLC <> :::'λ'_x_'..'_x_'·'_x not
R13436:13439 untypedLC <> :::'λ'_x_'..'_x_'·'_x not
R13466:13470 untypedLC <> subst def
R13512:13512 untypedLC <> F var
def 13611:13617 <> beta_at
R13642:13645 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R13646:13649 untypedLC <> lexp ind
R13632:13638 untypedLC <> rocc_of def
R13640:13641 untypedLC <> ex var
R13654:13665 untypedLC <> rewrite_at_g def
R13671:13680 untypedLC <> root_subst def
R13667:13669 untypedLC <> rar def
def 13704:13708 <> lift1
R13717:13720 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R13721:13723 untypedLC <> occ ind
R13714:13716 untypedLC <> occ ind
R13734:13737 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R13738:13741 untypedLC <> lexp ind
R13730:13733 untypedLC <> lexp ind
R13748:13748 Coq.Init.Logic <> ::type_scope:x_'->'_x not