-
Notifications
You must be signed in to change notification settings - Fork 0
/
STLC.glob
2001 lines (2001 loc) · 74.9 KB
/
STLC.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 1dfa8c7635d2d5c7be222fa2afe058c7
FSTLC
R15:29 Coq.Arith.EqNat <> <> lib
R47:71 Coq.Structures.Equalities <> <> lib
R89:102 Coq.Lists.List <> <> lib
R120:142 Coq.MSets.MSetInterface <> <> lib
R160:181 Coq.MSets.MSetWeakList <> <> lib
R199:222 Coq.Logic.Classical_Prop <> <> lib
R240:259 Coq.Program.Equality <> <> lib
R277:294 Coq.Arith.PeanoNat <> <> lib
R312:325 Coq.MSets.MSetProperties <> <> lib
R343:357 Coq.Init.Specif <> <> lib
R396:416 Coq.Structures.Equalities BooleanDecidableType' <> mod
R440:454 Coq.MSets.MSetInterface S <> mod
mod 368:370 <> TLC
R477:493 Coq.Structures.Equalities BoolEqualityFacts <> modtype
R495:500 STLC VarTyp <> modtype
mod 466:472 <> TLC.EqFacts
R517:533 Coq.MSets.MSetWeakList Make <> modtype
R535:540 STLC VarTyp <> modtype
mod 512:512 <> TLC.M
R582:594 Coq.MSets.MSetProperties WPropertiesOn <> modtype
R596:601 STLC VarTyp <> modtype
R604:604 STLC TLC.M <> modtype
mod 564:577 <> TLC.MSetProperties
ind 619:622 TLC STyp
constr 631:637 TLC STUnitT
constr 650:654 TLC STInt
constr 667:671 TLC STFun
constr 700:706 TLC STTuple
R641:644 STLC <> STyp ind
R658:661 STLC <> STyp ind
R679:682 Coq.Init.Logic <> :type_scope:x_'->'_x not
R687:690 Coq.Init.Logic <> :type_scope:x_'->'_x not
R691:694 STLC <> STyp ind
R683:686 STLC <> STyp ind
R675:678 STLC <> STyp ind
R714:717 Coq.Init.Logic <> :type_scope:x_'->'_x not
R722:725 Coq.Init.Logic <> :type_scope:x_'->'_x not
R726:729 STLC <> STyp ind
R718:721 STLC <> STyp ind
R710:713 STLC <> STyp ind
ind 743:746 TLC SExp
constr 766:771 TLC STFVar
constr 792:797 TLC STBVar
constr 820:825 TLC STUnit
constr 841:845 TLC STLit
constr 869:873 TLC STLam
constr 908:913 TLC STLam'
constr 939:943 TLC STApp
constr 980:985 TLC STPair
constr 1021:1027 TLC STProj1
constr 1052:1058 TLC STProj2
R777:780 Coq.Init.Logic <> :type_scope:x_'->'_x not
R781:784 STLC <> SExp ind
R786:786 STLC <> A var
R776:776 STLC <> A var
R805:808 Coq.Init.Logic <> :type_scope:x_'->'_x not
R809:812 STLC <> SExp ind
R814:814 STLC <> A var
R802:804 Coq.Init.Datatypes <> nat ind
R830:833 STLC <> SExp ind
R835:835 STLC <> A var
R854:857 Coq.Init.Logic <> :type_scope:x_'->'_x not
R858:861 STLC <> SExp ind
R863:863 STLC <> A var
R851:853 Coq.Init.Datatypes <> nat ind
R883:886 Coq.Init.Logic <> :type_scope:x_'->'_x not
R893:896 Coq.Init.Logic <> :type_scope:x_'->'_x not
R897:900 STLC <> SExp ind
R902:902 STLC <> A var
R887:890 STLC <> SExp ind
R892:892 STLC <> A var
R879:882 STLC TLC STyp ind
R924:927 Coq.Init.Logic <> :type_scope:x_'->'_x not
R928:931 STLC <> SExp ind
R933:933 STLC <> A var
R918:921 STLC <> SExp ind
R923:923 STLC <> A var
R955:958 Coq.Init.Logic <> :type_scope:x_'->'_x not
R965:968 Coq.Init.Logic <> :type_scope:x_'->'_x not
R969:972 STLC <> SExp ind
R974:974 STLC <> A var
R959:962 STLC <> SExp ind
R964:964 STLC <> A var
R949:952 STLC <> SExp ind
R954:954 STLC <> A var
R996:999 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1006:1009 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1010:1013 STLC <> SExp ind
R1015:1015 STLC <> A var
R1000:1003 STLC <> SExp ind
R1005:1005 STLC <> A var
R990:993 STLC <> SExp ind
R995:995 STLC <> A var
R1037:1040 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1041:1044 STLC <> SExp ind
R1046:1046 STLC <> A var
R1031:1034 STLC <> SExp ind
R1036:1036 STLC <> A var
R1068:1071 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1072:1075 STLC <> SExp ind
R1077:1077 STLC <> A var
R1062:1065 STLC <> SExp ind
R1067:1067 STLC <> A var
def 1092:1094 TLC Exp
R1109:1112 STLC TLC SExp ind
R1114:1114 STLC <> A var
def 1129:1131 TLC var
R1143:1150 STLC VarTyp t defax
def 1165:1168 TLC vars
R1173:1175 STLC TLC t def
def 1254:1260 TLC context
R1276:1279 Coq.Init.Datatypes <> list ind
R1285:1287 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
R1282:1284 STLC TLC var def
R1288:1288 STLC <> A var
def 1305:1310 TLC extend
R1321:1323 STLC TLC var def
R1331:1331 STLC <> A var
R1339:1345 STLC TLC context def
R1347:1347 STLC <> A var
R1352:1358 STLC TLC context def
R1360:1360 STLC <> A var
R1367:1367 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R1380:1384 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R1373:1376 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R1368:1368 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1370:1370 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1372:1372 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1369:1369 STLC <> x var
R1371:1371 STLC <> a var
R1377:1379 Coq.Init.Datatypes <> nil constr
R1385:1385 STLC <> c var
def 1400:1402 TLC dom
R1413:1419 STLC TLC context def
R1421:1421 STLC <> A var
R1426:1429 STLC TLC vars def
R1436:1445 Coq.Lists.List <> fold_right def
R1482:1482 STLC <> c var
R1476:1480 STLC TLC empty def
R1460:1462 STLC TLC add def
R1473:1473 STLC <> r var
R1465:1467 Coq.Init.Datatypes <> fst def
R1469:1470 STLC <> el var
def 1525:1530 TLC mapctx
R1544:1547 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1548:1548 STLC <> B var
R1543:1543 STLC <> A var
R1556:1562 STLC TLC context def
R1564:1564 STLC <> A var
R1569:1575 STLC TLC context def
R1577:1577 STLC <> B var
R1584:1586 Coq.Lists.List <> map def
R1620:1620 STLC <> c var
R1598:1598 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1604:1606 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1616:1617 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1599:1601 Coq.Init.Datatypes <> fst def
R1603:1603 STLC <> p var
R1607:1607 STLC <> f var
R1610:1612 Coq.Init.Datatypes <> snd def
R1614:1614 STLC <> p var
prf 1630:1641 TLC cons_to_push
R1665:1671 STLC TLC context def
R1673:1673 STLC <> A var
R1690:1692 Coq.Init.Logic <> :type_scope:x_'='_x not
R1685:1688 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R1679:1679 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1681:1682 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1684:1684 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R1680:1680 STLC <> x var
R1683:1683 STLC <> v var
R1689:1689 STLC <> E var
R1693:1698 STLC TLC extend def
R1704:1704 STLC <> E var
R1702:1702 STLC <> v var
R1700:1700 STLC <> x var
R1729:1734 STLC TLC extend def
prf 1773:1779 TLC env_ind
R1808:1811 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1799:1805 STLC TLC context def
R1807:1807 STLC <> A var
R1821:1821 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1827:1833 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1834:1834 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1872:1879 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1893:1893 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1890:1890 STLC <> P var
R1892:1892 STLC <> E var
R1852:1855 Coq.Init.Logic <> :type_scope:x_'->'_x not
R1856:1856 STLC <> P var
R1859:1864 STLC TLC extend def
R1870:1870 STLC <> E var
R1868:1868 STLC <> v var
R1866:1866 STLC <> x var
R1849:1849 STLC <> P var
R1851:1851 STLC <> E var
R1822:1822 STLC <> P var
R1824:1826 Coq.Init.Datatypes <> nil constr
R1912:1917 STLC TLC extend def
prf 2018:2027 TLC dom_map_id
R2056:2062 STLC TLC context def
R2064:2064 STLC <> A var
R2073:2076 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2077:2077 STLC <> B var
R2072:2072 STLC <> A var
R2088:2090 Coq.Init.Logic <> :type_scope:x_'='_x not
R2083:2085 STLC TLC dom def
R2087:2087 STLC <> E var
R2091:2093 STLC TLC dom def
R2096:2101 STLC TLC mapctx def
R2105:2105 STLC <> E var
R2103:2103 STLC <> f var
R2125:2130 STLC TLC mapctx def
prf 2240:2248 TLC dom_union
R2277:2283 STLC TLC context def
R2285:2285 STLC <> A var
R2314:2318 Coq.Init.Logic <> :type_scope:x_'<->'_x not
R2293:2296 STLC TLC In def
R2301:2303 STLC TLC dom def
R2307:2310 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R2306:2306 STLC <> E var
R2311:2311 STLC <> G var
R2298:2298 STLC <> x var
R2319:2322 STLC TLC In def
R2327:2333 STLC TLC union def
R2344:2346 STLC TLC dom def
R2348:2348 STLC <> G var
R2336:2338 STLC TLC dom def
R2340:2340 STLC <> E var
R2324:2324 STLC <> x var
R2426:2428 STLC TLC dom def
R2452:2456 Coq.Init.Logic <> iff def
R2484:2511 STLC TLC union_3 thm
R2484:2511 STLC TLC union_3 thm
R2536:2563 STLC TLC union_1 thm
R2536:2563 STLC TLC union_1 thm
R2685:2691 Coq.Init.Specif <> sumbool ind
R2710:2712 Coq.Init.Logic <> not def
R2715:2723 STLC VarTyp eq defax
R2694:2702 STLC VarTyp eq defax
R2741:2753 STLC VarTyp eq_dec defax
R2685:2691 Coq.Init.Specif <> sumbool ind
R2710:2712 Coq.Init.Logic <> not def
R2715:2723 STLC VarTyp eq defax
R2694:2702 STLC VarTyp eq defax
R2741:2753 STLC VarTyp eq_dec defax
R2779:2806 STLC TLC union_2 thm
R2779:2806 STLC TLC union_2 thm
R2817:2844 STLC TLC add_iff thm
R2817:2844 STLC TLC add_iff thm
R2866:2897 STLC TLC add_neq_iff thm
R2866:2897 STLC TLC add_neq_iff thm
R2866:2897 STLC TLC add_neq_iff thm
R2925:2931 STLC TLC Equal def
R2970:2974 STLC TLC add def
R2979:2985 STLC TLC union def
R2996:2998 STLC TLC dom def
R2988:2990 STLC TLC dom def
R2934:2940 STLC TLC union def
R2961:2963 STLC TLC dom def
R2943:2947 STLC TLC add def
R2952:2954 STLC TLC dom def
R3015:3038 STLC TLC union_add thm
R2925:2931 STLC TLC Equal def
R2970:2974 STLC TLC add def
R2979:2985 STLC TLC union def
R2996:2998 STLC TLC dom def
R2988:2990 STLC TLC dom def
R2934:2940 STLC TLC union def
R2961:2963 STLC TLC dom def
R2943:2947 STLC TLC add def
R2952:2954 STLC TLC dom def
R3015:3038 STLC TLC union_add thm
R3080:3082 Coq.Init.Logic <> not def
R3098:3123 STLC TLC add_2 thm
R3098:3123 STLC TLC add_2 thm
R3162:3189 STLC TLC union_1 thm
R3162:3189 STLC TLC union_1 thm
R3226:3232 Coq.Init.Specif <> sumbool ind
R3251:3253 Coq.Init.Logic <> not def
R3256:3264 STLC VarTyp eq defax
R3235:3243 STLC VarTyp eq defax
R3282:3294 STLC VarTyp eq_dec defax
R3226:3232 Coq.Init.Specif <> sumbool ind
R3251:3253 Coq.Init.Logic <> not def
R3256:3264 STLC VarTyp eq defax
R3235:3243 STLC VarTyp eq defax
R3282:3294 STLC VarTyp eq_dec defax
R3320:3347 STLC TLC add_iff thm
R3320:3347 STLC TLC add_iff thm
R3367:3398 STLC TLC add_neq_iff thm
R3367:3398 STLC TLC add_neq_iff thm
R3367:3398 STLC TLC add_neq_iff thm
R3419:3450 STLC TLC add_neq_iff thm
R3419:3450 STLC TLC add_neq_iff thm
R3480:3507 STLC TLC union_2 thm
R3480:3507 STLC TLC union_2 thm
R3530:3557 STLC TLC add_iff thm
R3530:3557 STLC TLC add_iff thm
R3590:3617 STLC TLC union_3 thm
R3590:3617 STLC TLC union_3 thm
prf 3648:3658 TLC list_impl_m
R3686:3686 STLC <> A var
R3710:3713 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3714:3717 STLC TLC In def
R3722:3724 STLC TLC dom def
R3726:3730 STLC <> Gamma var
R3719:3719 STLC <> x var
R3690:3696 Coq.Lists.List <> In def
R3705:3709 STLC <> Gamma var
R3698:3698 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3700:3701 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3703:3703 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3699:3699 STLC <> x var
R3702:3702 STLC <> v var
R3845:3870 STLC TLC add_1 thm
R3845:3870 STLC TLC add_1 thm
R3900:3902 Coq.Init.Datatypes <> fst def
R3881:3887 Coq.Init.Logic <> f_equal thm
R3900:3902 Coq.Init.Datatypes <> fst def
R3881:3887 Coq.Init.Logic <> f_equal thm
R3964:3989 STLC TLC add_2 thm
R3964:3989 STLC TLC add_2 thm
R4067:4075 STLC TLC dom_union thm
R4093:4104 STLC TLC union_spec thm
R4141:4144 STLC TLC In def
R4148:4154 STLC TLC empty def
R4141:4144 STLC TLC In def
R4148:4154 STLC TLC empty def
R4198:4201 STLC TLC In def
R4206:4208 STLC TLC dom def
R4210:4212 Coq.Init.Datatypes <> nil constr
R4198:4201 STLC TLC In def
R4206:4208 STLC TLC dom def
R4210:4212 Coq.Init.Datatypes <> nil constr
R4247:4250 STLC TLC In def
R4255:4257 STLC TLC dom def
R4268:4271 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R4260:4260 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4263:4264 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4267:4267 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4247:4250 STLC TLC In def
R4255:4257 STLC TLC dom def
R4268:4271 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R4260:4260 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4263:4264 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4267:4267 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4348:4351 STLC TLC In def
R4357:4359 STLC TLC dom def
R4369:4372 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R4362:4362 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4364:4365 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4368:4368 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4348:4351 STLC TLC In def
R4357:4359 STLC TLC dom def
R4369:4372 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R4362:4362 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4364:4365 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4368:4368 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4436:4437 Coq.Init.Logic <> :type_scope:'~'_x not
R4436:4437 Coq.Init.Logic <> :type_scope:'~'_x not
R4480:4481 Coq.Init.Logic <> :type_scope:'~'_x not
R4482:4485 STLC TLC In def
R4491:4501 STLC TLC singleton def
R4480:4481 Coq.Init.Logic <> :type_scope:'~'_x not
R4482:4485 STLC TLC In def
R4491:4501 STLC TLC singleton def
R4509:4511 Coq.Init.Logic <> not def
R4514:4522 STLC VarTyp eq defax
R4509:4511 Coq.Init.Logic <> not def
R4514:4522 STLC VarTyp eq defax
R4603:4604 Coq.Init.Logic <> :type_scope:'~'_x not
R4605:4608 STLC TLC In def
R4613:4623 STLC TLC singleton def
R4603:4604 Coq.Init.Logic <> :type_scope:'~'_x not
R4605:4608 STLC TLC In def
R4613:4623 STLC TLC singleton def
R4632:4634 Coq.Init.Logic <> not def
R4637:4645 STLC VarTyp eq defax
R4632:4634 Coq.Init.Logic <> not def
R4637:4645 STLC VarTyp eq defax
R4764:4765 Coq.Init.Logic <> :type_scope:'~'_x not
R4766:4769 STLC TLC In def
R4774:4778 STLC TLC add def
R4783:4789 STLC TLC empty def
R4764:4765 Coq.Init.Logic <> :type_scope:'~'_x not
R4766:4769 STLC TLC In def
R4774:4778 STLC TLC add def
R4783:4789 STLC TLC empty def
R4861:4863 Coq.Init.Logic <> not def
R4866:4869 STLC TLC In def
R4874:4876 STLC TLC dom def
R4861:4863 Coq.Init.Logic <> not def
R4866:4869 STLC TLC In def
R4874:4876 STLC TLC dom def
R4935:4937 Coq.Init.Logic <> not def
R4940:4943 STLC TLC In def
R4948:4954 STLC TLC union def
R4935:4937 Coq.Init.Logic <> not def
R4940:4943 STLC TLC In def
R4948:4954 STLC TLC union def
R5015:5017 Coq.Init.Logic <> not def
R5030:5033 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5020:5023 STLC TLC In def
R5015:5017 Coq.Init.Logic <> not def
R5030:5033 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5020:5023 STLC TLC In def
R5152:5154 Coq.Init.Logic <> not def
R5159:5162 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5163:5166 STLC TLC In def
R5152:5154 Coq.Init.Logic <> not def
R5159:5162 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5163:5166 STLC TLC In def
R5289:5291 Coq.Init.Logic <> not def
R5294:5297 STLC TLC In def
R5289:5291 Coq.Init.Logic <> not def
R5294:5297 STLC TLC In def
R5309:5311 Coq.Init.Logic <> not def
R5314:5317 STLC TLC In def
R5309:5311 Coq.Init.Logic <> not def
R5314:5317 STLC TLC In def
R5353:5355 Coq.Init.Logic <> :type_scope:'~'_x not
R5377:5377 Coq.Init.Logic <> :type_scope:'~'_x not
R5363:5366 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5357:5360 Coq.Structures.Equalities EqNotation ::x_'=='_x not
R5367:5370 STLC TLC In def
R5353:5355 Coq.Init.Logic <> :type_scope:'~'_x not
R5377:5377 Coq.Init.Logic <> :type_scope:'~'_x not
R5363:5366 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5357:5360 Coq.Structures.Equalities EqNotation ::x_'=='_x not
R5367:5370 STLC TLC In def
R5447:5449 Coq.Init.Logic <> not def
R5454:5457 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5447:5449 Coq.Init.Logic <> not def
R5454:5457 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5499:5500 Coq.Init.Logic <> :type_scope:'~'_x not
R5501:5504 STLC TLC In def
R5509:5519 STLC TLC singleton def
R5499:5500 Coq.Init.Logic <> :type_scope:'~'_x not
R5501:5504 STLC TLC In def
R5509:5519 STLC TLC singleton def
R5532:5535 Coq.Structures.Equalities EqNotation ::x_'=='_x not
R5532:5535 Coq.Structures.Equalities EqNotation ::x_'=='_x not
R5626:5627 Coq.Init.Logic <> :type_scope:'~'_x not
R5628:5631 STLC TLC In def
R5636:5646 STLC TLC singleton def
R5626:5627 Coq.Init.Logic <> :type_scope:'~'_x not
R5628:5631 STLC TLC In def
R5636:5646 STLC TLC singleton def
R5658:5661 Coq.Structures.Equalities EqNotation ::x_'=='_x not
R5658:5661 Coq.Structures.Equalities EqNotation ::x_'=='_x not
R5762:5764 Coq.Init.Logic <> not def
R5767:5770 STLC TLC In def
R5762:5764 Coq.Init.Logic <> not def
R5767:5770 STLC TLC In def
R5782:5784 Coq.Init.Logic <> not def
R5787:5790 STLC TLC In def
R5782:5784 Coq.Init.Logic <> not def
R5787:5790 STLC TLC In def
R5815:5817 Coq.Init.Logic <> not def
R5852:5863 STLC TLC union_spec thm
R5698:5729 STLC TLC singleton_2 thm
R5571:5602 STLC TLC singleton_2 thm
R5471:5480 Coq.Logic.Classical_Prop <> and_not_or thm
R5389:5391 Coq.Init.Logic <> not def
R5243:5252 Coq.Logic.Classical_Prop <> not_or_and thm
R5106:5115 Coq.Logic.Classical_Prop <> not_or_and thm
R4988:4999 STLC TLC union_spec thm
R4899:4907 STLC TLC dom_union thm
R4811:4844 STLC TLC singleton_equal_add thm
R4664:4697 STLC TLC singleton_iff thm
R4712:4714 Coq.Init.Logic <> not def
R4541:4574 STLC TLC singleton_iff thm
R4397:4424 STLC TLC add_iff thm
R4296:4323 STLC TLC add_iff thm
ind 5903:5904 TLC ok
constr 5937:5942 TLC Ok_nil
constr 5957:5963 TLC Ok_push
R5921:5924 Coq.Init.Logic <> :type_scope:x_'->'_x not
R5912:5918 STLC TLC context def
R5946:5947 STLC <> ok ind
R5949:5951 Coq.Init.Datatypes <> nil constr
R5946:5947 STLC <> A var
R5979:5985 STLC TLC context def
R5987:5987 STLC <> A var
R5995:5997 STLC TLC var def
R6006:6006 STLC <> A var
R6030:6033 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6052:6055 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6056:6057 STLC <> ok ind
R6060:6065 STLC TLC extend def
R6072:6072 STLC <> E var
R6069:6070 STLC <> ty var
R6067:6067 STLC <> v var
R6056:6057 STLC <> A var
R6034:6036 Coq.Init.Logic <> not def
R6039:6040 STLC TLC In def
R6045:6047 STLC TLC dom def
R6049:6049 STLC <> E var
R6042:6042 STLC <> v var
R6026:6027 STLC <> ok ind
R6029:6029 STLC <> E var
R6026:6027 STLC <> A var
R6103:6104 STLC <> ok ind
prf 6114:6121 TLC ok_app_l
R6143:6149 STLC TLC context def
R6151:6151 STLC <> A var
R6166:6169 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6170:6171 STLC TLC ok ind
R6173:6173 STLC <> E var
R6155:6156 STLC TLC ok ind
R6160:6163 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R6159:6159 STLC <> E var
R6164:6164 STLC <> F var
R6226:6231 STLC TLC Ok_nil constr
R6226:6231 STLC TLC Ok_nil constr
R6266:6272 STLC TLC Ok_push constr
R6266:6272 STLC TLC Ok_push constr
prf 6329:6336 TLC ok_app_r
R6358:6364 STLC TLC context def
R6366:6366 STLC <> A var
R6381:6384 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6385:6386 STLC TLC ok ind
R6388:6388 STLC <> F var
R6370:6371 STLC TLC ok ind
R6375:6378 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R6374:6374 STLC <> E var
R6379:6379 STLC <> F var
R6447:6455 Coq.Lists.List <> app_nil_l thm
R6447:6455 Coq.Lists.List <> app_nil_l thm
R6447:6455 Coq.Lists.List <> app_nil_l thm
prf 6535:6543 TLC ok_remove
R6567:6573 STLC TLC context def
R6575:6575 STLC <> A var
R6595:6598 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6599:6600 STLC TLC ok ind
R6604:6607 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R6603:6603 STLC <> E var
R6608:6608 STLC <> F var
R6579:6580 STLC TLC ok ind
R6584:6587 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R6583:6583 STLC <> E var
R6589:6592 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R6588:6588 STLC <> G var
R6593:6593 STLC <> F var
R6649:6655 STLC TLC env_ind thm
R6649:6655 STLC TLC env_ind thm
R6668:6676 Coq.Lists.List <> app_nil_l thm
R6668:6676 Coq.Lists.List <> app_nil_l thm
R6668:6676 Coq.Lists.List <> app_nil_l thm
R6696:6703 STLC TLC ok_app_r thm
R6696:6703 STLC TLC ok_app_r thm
R6720:6725 STLC TLC extend def
R6739:6747 Coq.Lists.List <> app_assoc thm
R6739:6747 Coq.Lists.List <> app_assoc thm
R6739:6747 Coq.Lists.List <> app_assoc thm
R6758:6764 STLC TLC Ok_push constr
R6758:6764 STLC TLC Ok_push constr
R6789:6794 STLC TLC extend def
R6813:6821 Coq.Lists.List <> app_assoc thm
R6813:6821 Coq.Lists.List <> app_assoc thm
R6813:6821 Coq.Lists.List <> app_assoc thm
R6874:6879 STLC TLC extend def
R6919:6927 STLC TLC dom_union thm
R6919:6927 STLC TLC dom_union thm
R6919:6927 STLC TLC dom_union thm
R6945:6954 STLC TLC union_spec thm
R6945:6954 STLC TLC union_spec thm
R6945:6954 STLC TLC union_spec thm
R6971:6973 Coq.Init.Logic <> not def
R7039:7047 STLC TLC dom_union thm
R7058:7067 STLC TLC union_spec thm
R7039:7047 STLC TLC dom_union thm
R7039:7047 STLC TLC dom_union thm
R7058:7067 STLC TLC union_spec thm
R7058:7067 STLC TLC union_spec thm
prf 7096:7109 TLC ok_extend_comm
R7131:7137 STLC TLC context def
R7139:7139 STLC <> A var
R7190:7208 Coq.Init.Logic <> :type_scope:x_'->'_x not
R7209:7210 STLC TLC ok ind
R7214:7217 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R7213:7213 STLC <> F var
R7224:7227 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R7218:7218 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R7220:7221 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R7223:7223 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R7219:7219 STLC <> x var
R7222:7222 STLC <> v var
R7231:7234 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R7228:7230 Coq.Init.Datatypes <> nil constr
R7235:7235 STLC <> E var
R7162:7163 STLC TLC ok ind
R7167:7170 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R7166:7166 STLC <> F var
R7172:7175 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R7171:7171 STLC <> E var
R7182:7185 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R7176:7176 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R7178:7179 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R7181:7181 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R7177:7177 STLC <> x var
R7180:7180 STLC <> v var
R7186:7188 Coq.Init.Datatypes <> nil constr
R7321:7327 STLC TLC env_ind thm
R7321:7327 STLC TLC env_ind thm
R7347:7352 STLC TLC extend def
R7372:7380 Coq.Lists.List <> app_nil_l thm
R7372:7380 Coq.Lists.List <> app_nil_l thm
R7372:7380 Coq.Lists.List <> app_nil_l thm
R7398:7404 STLC TLC Ok_push constr
R7398:7404 STLC TLC Ok_push constr
R7419:7426 STLC TLC ok_app_l thm
R7419:7426 STLC TLC ok_app_l thm
R7460:7462 Coq.Init.Logic <> not def
R7516:7528 Coq.Lists.List <> app_comm_cons thm
R7516:7528 Coq.Lists.List <> app_comm_cons thm
R7516:7528 Coq.Lists.List <> app_comm_cons thm
R7604:7606 Coq.Init.Logic <> not def
R7626:7653 STLC TLC add_iff thm
R7626:7653 STLC TLC add_iff thm
R7707:7715 STLC TLC dom_union thm
R7707:7715 STLC TLC dom_union thm
R7707:7715 STLC TLC dom_union thm
R7734:7743 STLC TLC union_spec thm
R7734:7743 STLC TLC union_spec thm
R7734:7743 STLC TLC union_spec thm
R7760:7769 Coq.Logic.Classical_Prop <> not_or_and thm
R7760:7769 Coq.Logic.Classical_Prop <> not_or_and thm
R7829:7854 STLC TLC add_1 thm
R7829:7854 STLC TLC add_1 thm
R7898:7903 STLC TLC extend def
R7919:7927 Coq.Lists.List <> app_assoc thm
R7919:7927 Coq.Lists.List <> app_assoc thm
R7919:7927 Coq.Lists.List <> app_assoc thm
R7938:7944 STLC TLC Ok_push constr
R7938:7944 STLC TLC Ok_push constr
R8010:8018 STLC TLC dom_union thm
R8010:8018 STLC TLC dom_union thm
R8010:8018 STLC TLC dom_union thm
R8031:8040 STLC TLC union_spec thm
R8031:8040 STLC TLC union_spec thm
R8031:8040 STLC TLC union_spec thm
R8052:8054 Coq.Init.Logic <> not def
R8088:8095 STLC TLC ok_app_l thm
R8088:8095 STLC TLC ok_app_l thm
R8171:8198 STLC TLC add_iff thm
R8171:8198 STLC TLC add_iff thm
R8232:8237 STLC TLC extend def
R8255:8263 STLC TLC ok_remove thm
R8255:8263 STLC TLC ok_remove thm
R8286:8294 Coq.Lists.List <> app_assoc thm
R8286:8294 Coq.Lists.List <> app_assoc thm
R8286:8294 Coq.Lists.List <> app_assoc thm
R8312:8320 STLC TLC ok_remove thm
R8312:8320 STLC TLC ok_remove thm
R8404:8429 STLC TLC add_1 thm
R8404:8429 STLC TLC add_1 thm
R8480:8488 STLC TLC dom_union thm
R8505:8514 STLC TLC union_spec thm
R8480:8488 STLC TLC dom_union thm
R8480:8488 STLC TLC dom_union thm
R8505:8514 STLC TLC union_spec thm
R8505:8514 STLC TLC union_spec thm
R8531:8540 Coq.Logic.Classical_Prop <> not_or_and thm
R8531:8540 Coq.Logic.Classical_Prop <> not_or_and thm
R8575:8583 STLC TLC dom_union thm
R8600:8609 STLC TLC union_spec thm
R8624:8633 Coq.Logic.Classical_Prop <> not_or_and thm
R8575:8583 STLC TLC dom_union thm
R8575:8583 STLC TLC dom_union thm
R8600:8609 STLC TLC union_spec thm
R8600:8609 STLC TLC union_spec thm
R8624:8633 Coq.Logic.Classical_Prop <> not_or_and thm
prf 8693:8703 TLC ok_app_comm
R8725:8731 STLC TLC context def
R8733:8733 STLC <> A var
R8748:8751 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8752:8753 STLC TLC ok ind
R8757:8760 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R8756:8756 STLC <> E var
R8761:8761 STLC <> F var
R8737:8738 STLC TLC ok ind
R8742:8745 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R8741:8741 STLC <> F var
R8746:8746 STLC <> E var
R8866:8872 STLC TLC env_ind thm
R8866:8872 STLC TLC env_ind thm
R8898:8906 Coq.Lists.List <> app_nil_r thm
R8898:8906 Coq.Lists.List <> app_nil_r thm
R8898:8906 Coq.Lists.List <> app_nil_r thm
R8946:8951 STLC TLC extend def
R8972:8980 Coq.Lists.List <> app_assoc thm
R8972:8980 Coq.Lists.List <> app_assoc thm
R8972:8980 Coq.Lists.List <> app_assoc thm
R8991:8997 STLC TLC Ok_push constr
R8991:8997 STLC TLC Ok_push constr
R9021:9029 STLC TLC ok_remove thm
R9021:9029 STLC TLC ok_remove thm
R9061:9069 STLC TLC dom_union thm
R9061:9069 STLC TLC dom_union thm
R9061:9069 STLC TLC dom_union thm
R9082:9091 STLC TLC union_spec thm
R9082:9091 STLC TLC union_spec thm
R9082:9091 STLC TLC union_spec thm
R9103:9105 Coq.Init.Logic <> not def
R9140:9147 STLC TLC ok_app_r thm
R9140:9147 STLC TLC ok_app_r thm
R9204:9212 Coq.Lists.List <> app_assoc thm
R9204:9212 Coq.Lists.List <> app_assoc thm
R9204:9212 Coq.Lists.List <> app_assoc thm
R9228:9235 STLC TLC ok_app_l thm
R9228:9235 STLC TLC ok_app_l thm
R9256:9264 Coq.Lists.List <> app_nil_l thm
R9256:9264 Coq.Lists.List <> app_nil_l thm
R9256:9264 Coq.Lists.List <> app_nil_l thm
R9280:9293 STLC TLC ok_extend_comm thm
R9280:9293 STLC TLC ok_extend_comm thm
R9311:9319 Coq.Lists.List <> app_nil_l thm
R9311:9319 Coq.Lists.List <> app_nil_l thm
R9311:9319 Coq.Lists.List <> app_nil_l thm
def 9405:9414 TLC ok_app_and
R9427:9433 STLC TLC context def
R9435:9435 STLC <> A var
R9443:9444 STLC TLC ok ind
R9448:9451 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9447:9447 STLC <> E var
R9452:9452 STLC <> F var
R9462:9465 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9458:9459 STLC TLC ok ind
R9461:9461 STLC <> E var
R9466:9467 STLC TLC ok ind
R9469:9469 STLC <> F var
R9476:9479 Coq.Init.Logic <> conj constr
R9499:9506 STLC TLC ok_app_r thm
R9512:9512 STLC <> H var
R9482:9489 STLC TLC ok_app_l thm
R9495:9495 STLC <> H var
prf 9523:9536 TLC ok_middle_comm
R9558:9564 STLC TLC context def
R9566:9566 STLC <> A var
R9597:9600 Coq.Init.Logic <> :type_scope:x_'->'_x not
R9601:9602 STLC TLC ok ind
R9606:9609 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9605:9605 STLC <> E var
R9611:9614 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9610:9610 STLC <> G var
R9616:9619 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9615:9615 STLC <> F var
R9620:9620 STLC <> H var
R9576:9577 STLC TLC ok ind
R9581:9584 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9580:9580 STLC <> E var
R9586:9589 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9585:9585 STLC <> F var
R9591:9594 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R9590:9590 STLC <> G var
R9595:9595 STLC <> H var
R9715:9723 Coq.Lists.List <> app_nil_l thm
R9715:9723 Coq.Lists.List <> app_nil_l thm
R9715:9723 Coq.Lists.List <> app_nil_l thm
R9741:9749 Coq.Lists.List <> app_nil_r thm
R9741:9749 Coq.Lists.List <> app_nil_r thm
R9741:9749 Coq.Lists.List <> app_nil_r thm
R9769:9779 STLC TLC ok_app_comm thm
R9769:9779 STLC TLC ok_app_comm thm
R9792:9800 Coq.Lists.List <> app_nil_l thm
R9792:9800 Coq.Lists.List <> app_nil_l thm
R9792:9800 Coq.Lists.List <> app_nil_l thm
R9813:9821 Coq.Lists.List <> app_assoc thm
R9813:9821 Coq.Lists.List <> app_assoc thm
R9813:9821 Coq.Lists.List <> app_assoc thm
R9832:9842 STLC TLC ok_app_comm thm
R9832:9842 STLC TLC ok_app_comm thm
R9858:9870 Coq.Lists.List <> app_comm_cons thm
R9858:9870 Coq.Lists.List <> app_comm_cons thm
R9858:9870 Coq.Lists.List <> app_comm_cons thm
R9895:9901 STLC TLC Ok_push constr
R9895:9901 STLC TLC Ok_push constr
R9912:9922 STLC TLC ok_app_comm thm
R9912:9922 STLC TLC ok_app_comm thm
R9938:9946 Coq.Lists.List <> app_assoc thm
R9938:9946 Coq.Lists.List <> app_assoc thm
R9938:9946 Coq.Lists.List <> app_assoc thm
R9959:9967 Coq.Lists.List <> app_nil_l thm
R9959:9967 Coq.Lists.List <> app_nil_l thm
R9959:9967 Coq.Lists.List <> app_nil_l thm
R9986:9994 Coq.Lists.List <> app_assoc thm
R9986:9994 Coq.Lists.List <> app_assoc thm
R9986:9994 Coq.Lists.List <> app_assoc thm
R10011:10021 STLC TLC ok_app_comm thm
R10011:10021 STLC TLC ok_app_comm thm
R10043:10055 Coq.Lists.List <> app_comm_cons thm
R10043:10055 Coq.Lists.List <> app_comm_cons thm
R10043:10055 Coq.Lists.List <> app_comm_cons thm
R10113:10121 Coq.Lists.List <> app_nil_l thm
R10113:10121 Coq.Lists.List <> app_nil_l thm
R10113:10121 Coq.Lists.List <> app_nil_l thm
R10132:10142 STLC TLC ok_app_comm thm
R10132:10142 STLC TLC ok_app_comm thm
R10168:10176 Coq.Lists.List <> app_assoc thm
R10168:10176 Coq.Lists.List <> app_assoc thm
R10168:10176 Coq.Lists.List <> app_assoc thm
R10195:10203 Coq.Lists.List <> app_nil_l thm
R10195:10203 Coq.Lists.List <> app_nil_l thm
R10195:10203 Coq.Lists.List <> app_nil_l thm
R10222:10230 Coq.Lists.List <> app_assoc thm
R10222:10230 Coq.Lists.List <> app_assoc thm
R10222:10230 Coq.Lists.List <> app_assoc thm
R10247:10257 STLC TLC ok_app_comm thm
R10247:10257 STLC TLC ok_app_comm thm
R10279:10291 Coq.Lists.List <> app_comm_cons thm
R10279:10291 Coq.Lists.List <> app_comm_cons thm
R10279:10291 Coq.Lists.List <> app_comm_cons thm
R10347:10355 STLC TLC dom_union thm
R10372:10381 STLC TLC union_spec thm
R10347:10355 STLC TLC dom_union thm
R10347:10355 STLC TLC dom_union thm
R10372:10381 STLC TLC union_spec thm
R10372:10381 STLC TLC union_spec thm
R10442:10454 Coq.Lists.List <> app_comm_cons thm
R10442:10454 Coq.Lists.List <> app_comm_cons thm
R10442:10454 Coq.Lists.List <> app_comm_cons thm
R10479:10485 STLC TLC Ok_push constr
R10479:10485 STLC TLC Ok_push constr
R10514:10526 Coq.Lists.List <> app_comm_cons thm
R10514:10526 Coq.Lists.List <> app_comm_cons thm
R10514:10526 Coq.Lists.List <> app_comm_cons thm
R10578:10590 Coq.Lists.List <> app_comm_cons thm
R10578:10590 Coq.Lists.List <> app_comm_cons thm
R10578:10590 Coq.Lists.List <> app_comm_cons thm
R10648:10656 STLC TLC dom_union thm
R10673:10682 STLC TLC union_spec thm
R10648:10656 STLC TLC dom_union thm
R10648:10656 STLC TLC dom_union thm
R10673:10682 STLC TLC union_spec thm
R10673:10682 STLC TLC union_spec thm
R10732:10740 STLC TLC dom_union thm
R10757:10766 STLC TLC union_spec thm
R10732:10740 STLC TLC dom_union thm
R10732:10740 STLC TLC dom_union thm
R10757:10766 STLC TLC union_spec thm
R10757:10766 STLC TLC union_spec thm
def 10867:10868 TLC fv
R10878:10881 STLC TLC SExp ind
R10883:10885 STLC TLC var def
R10890:10893 STLC TLC vars def
R10906:10909 STLC <> sExp var
R10922:10927 STLC TLC STFVar constr
R10936:10944 STLC TLC singleton def
R10954:10959 STLC TLC STBVar constr
R10968:10972 STLC TLC empty def
R10980:10985 STLC TLC STUnit constr
R10992:10996 STLC TLC empty def
R11004:11008 STLC TLC STLit constr
R11017:11021 STLC TLC empty def
R11029:11033 STLC TLC STLam constr
R11044:11045 STLC <> fv def
R11055:11060 STLC TLC STLam' constr
R11069:11070 STLC <> fv def
R11080:11084 STLC TLC STApp constr
R11097:11101 STLC TLC union def
R11112:11113 STLC <> fv def
R11104:11105 STLC <> fv def
R11125:11130 STLC TLC STPair constr
R11143:11147 STLC TLC union def
R11158:11159 STLC <> fv def
R11150:11151 STLC <> fv def
R11171:11177 STLC TLC STProj1 constr
R11186:11187 STLC <> fv def
R11197:11203 STLC TLC STProj2 constr
R11212:11213 STLC <> fv def
def 11234:11241 TLC open_rec
R11248:11250 Coq.Init.Datatypes <> nat ind
R11258:11261 STLC TLC SExp ind
R11263:11265 STLC TLC var def
R11273:11276 STLC TLC SExp ind
R11278:11280 STLC TLC var def
R11296:11299 STLC TLC SExp ind
R11301:11303 STLC TLC var def
R11316:11316 STLC <> t var
R11327:11332 STLC TLC STBVar constr
R11344:11350 Coq.Arith.PeanoNat Nat eqb def
R11352:11352 STLC <> k var
R11369:11374 STLC TLC STBVar constr
R11361:11361 STLC <> u var
R11385:11390 STLC TLC STFVar constr
R11399:11404 STLC TLC STFVar constr
R11414:11419 STLC TLC STUnit constr
R11426:11431 STLC TLC STUnit constr
R11439:11443 STLC TLC STLit constr
R11452:11456 STLC TLC STLit constr
R11466:11470 STLC TLC STLam constr
R11483:11487 STLC TLC STLam constr
R11495:11502 STLC <> open_rec def
R11510:11510 STLC <> u var
R11505:11505 Coq.Init.Datatypes <> S constr
R11507:11507 STLC <> k var
R11520:11525 STLC TLC STLam' constr
R11535:11540 STLC TLC STLam' constr
R11545:11552 STLC <> open_rec def
R11560:11560 STLC <> u var
R11555:11555 Coq.Init.Datatypes <> S constr
R11557:11557 STLC <> k var
R11574:11578 STLC TLC STApp constr
R11591:11595 STLC TLC STApp constr
R11618:11625 STLC <> open_rec def
R11629:11629 STLC <> u var
R11627:11627 STLC <> k var
R11600:11607 STLC <> open_rec def
R11611:11611 STLC <> u var
R11609:11609 STLC <> k var
R11639:11644 STLC TLC STPair constr
R11657:11662 STLC TLC STPair constr
R11685:11692 STLC <> open_rec def
R11696:11696 STLC <> u var
R11694:11694 STLC <> k var
R11667:11674 STLC <> open_rec def
R11678:11678 STLC <> u var
R11676:11676 STLC <> k var
R11706:11712 STLC TLC STProj1 constr
R11721:11727 STLC TLC STProj1 constr
R11732:11739 STLC <> open_rec def
R11745:11745 STLC <> t var
R11743:11743 STLC <> u var
R11741:11741 STLC <> k var
R11752:11758 STLC TLC STProj2 constr
R11767:11773 STLC TLC STProj2 constr
R11778:11785 STLC <> open_rec def
R11791:11791 STLC <> t var
R11789:11789 STLC <> u var
R11787:11787 STLC <> k var
def 11813:11816 TLC open
R11823:11826 STLC TLC SExp ind
R11828:11830 STLC TLC var def
R11838:11845 STLC TLC open_rec def
R11851:11851 STLC <> t var
R11849:11849 STLC <> u var
R11945:11952 STLC TLC open_rec def
not 11926:11926 TLC ::'{'_x_'~>'_x_'}'_x
R11997:12000 STLC TLC open def
R12005:12010 STLC TLC STFVar constr
R12012:12014 STLC TLC var def
not 11985:11985 TLC ::x_'^'_x
R12043:12046 STLC TLC open def
not 12030:12030 TLC ::x_'^^'_x
prf 12075:12082 TLC fv_distr
R12134:12152 Coq.Init.Logic <> :type_scope:x_'->'_x not
R12153:12154 STLC TLC In def
R12159:12163 STLC TLC union def
R12174:12175 STLC TLC fv def
R12177:12178 STLC <> t2 var
R12166:12167 STLC TLC fv def
R12169:12170 STLC <> t1 var
R12156:12156 STLC <> x var
R12106:12107 STLC TLC In def
R12112:12113 STLC TLC fv def
R12116:12123 STLC TLC open_rec def
R12130:12131 STLC <> t1 var
R12127:12128 STLC <> t2 var
R12125:12125 STLC <> n var
R12109:12109 STLC <> x var
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12297:12306 STLC TLC union_spec thm
R12334:12340 Coq.Arith.PeanoNat Nat eqb def
R12334:12340 Coq.Arith.PeanoNat Nat eqb def
R12371:12380 STLC TLC union_spec thm
R12371:12380 STLC TLC union_spec thm
R12371:12380 STLC TLC union_spec thm
R12450:12459 STLC TLC union_spec thm
R12450:12459 STLC TLC union_spec thm
R12450:12459 STLC TLC union_spec thm
R12479:12488 STLC TLC union_spec thm
R12479:12488 STLC TLC union_spec thm
R12479:12488 STLC TLC union_spec thm
R12520:12526 Coq.Init.Logic <> or_comm thm
R12520:12526 Coq.Init.Logic <> or_comm thm
R12520:12526 Coq.Init.Logic <> or_comm thm
R12549:12556 Coq.Init.Logic <> or_assoc thm