-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathsubject_reduction.glob
2143 lines (2143 loc) · 95.9 KB
/
subject_reduction.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 fb1ea0cf7703b7b4d59d0fdf3f8767f9
Fsubject_reduction
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2015 Coq.Bool.Bool <> <> lib
R2033:2036 Coq.Lists.List <> <> lib
R2054:2060 General <> <> lib
R2078:2080 Coq.Arith.Max <> <> lib
R2099:2102 Test <> <> lib
R2120:2130 LamSF_Terms <> <> lib
R2148:2160 LamSF_Tactics <> <> lib
R2178:2200 LamSF_Substitution_term <> <> lib
R2218:2227 Components <> <> lib
R2245:2253 Compounds <> <> lib
R2271:2285 LamSF_reduction <> <> lib
R2303:2314 LamSF_Closed <> <> lib
R2332:2346 type_derivation <> <> lib
R2364:2383 type_derivation_resi <> <> lib
R2401:2419 type_derivation_rwf <> <> lib
R2437:2450 operator_types <> <> lib
R2598:2607 type_derivation <> derivation ind
R2615:2617 LamSF_Terms <> Abs constr
R2598:2607 type_derivation <> derivation ind
R2615:2617 LamSF_Terms <> Abs constr
R2661:2670 type_derivation <> derivation ind
R2675:2677 LamSF_Terms <> Ref constr
R2661:2670 type_derivation <> derivation ind
R2675:2677 LamSF_Terms <> Ref constr
R2713:2722 type_derivation <> derivation ind
R2727:2728 LamSF_Terms <> Op constr
R2730:2732 LamSF_Terms <> Sop constr
R2713:2722 type_derivation <> derivation ind
R2727:2728 LamSF_Terms <> Op constr
R2730:2732 LamSF_Terms <> Sop constr
R2775:2784 type_derivation <> derivation ind
R2789:2790 LamSF_Terms <> Op constr
R2792:2794 LamSF_Terms <> Aop constr
R2775:2784 type_derivation <> derivation ind
R2789:2790 LamSF_Terms <> Op constr
R2792:2794 LamSF_Terms <> Aop constr
R2837:2846 type_derivation <> derivation ind
R2851:2852 LamSF_Terms <> Op constr
R2854:2856 LamSF_Terms <> Kop constr
R2837:2846 type_derivation <> derivation ind
R2851:2852 LamSF_Terms <> Op constr
R2854:2856 LamSF_Terms <> Kop constr
R2899:2908 type_derivation <> derivation ind
R2913:2914 LamSF_Terms <> Op constr
R2916:2918 LamSF_Terms <> Eop constr
R2899:2908 type_derivation <> derivation ind
R2913:2914 LamSF_Terms <> Op constr
R2916:2918 LamSF_Terms <> Eop constr
R2961:2970 type_derivation <> derivation ind
R2975:2976 LamSF_Terms <> Op constr
R2978:2980 LamSF_Terms <> Gop constr
R2961:2970 type_derivation <> derivation ind
R2975:2976 LamSF_Terms <> Op constr
R2978:2980 LamSF_Terms <> Gop constr
R3023:3032 type_derivation <> derivation ind
R3037:3038 LamSF_Terms <> Op constr
R3040:3042 LamSF_Terms <> Yop constr
R3023:3032 type_derivation <> derivation ind
R3037:3038 LamSF_Terms <> Op constr
R3040:3042 LamSF_Terms <> Yop constr
R3085:3094 type_derivation <> derivation ind
R3098:3101 Components <> i_op def
R3085:3094 type_derivation <> derivation ind
R3098:3101 Components <> i_op def
R3143:3152 type_derivation <> derivation ind
R3157:3159 LamSF_Terms <> App constr
R3166:3169 Components <> i_op def
R3161:3164 Components <> k_op def
R3143:3152 type_derivation <> derivation ind
R3157:3159 LamSF_Terms <> App constr
R3166:3169 Components <> i_op def
R3161:3164 Components <> k_op def
R3213:3222 type_derivation <> derivation ind
R3227:3229 LamSF_Terms <> App constr
R3213:3222 type_derivation <> derivation ind
R3227:3229 LamSF_Terms <> App constr
R3286:3295 type_derivation <> derivation ind
R3300:3302 LamSF_Terms <> Abs constr
R3286:3295 type_derivation <> derivation ind
R3300:3302 LamSF_Terms <> Abs constr
R3319:3328 type_derivation <> derive_abs constr
R3248:3257 type_derivation <> derive_app constr
R2632:2642 type_derivation <> derive_gen1 constr
prf 3371:3380 <> derive_ops
R3488:3497 type_derivation <> derivation ind
R3508:3509 subject_reduction <> ty var
R3505:3506 subject_reduction <> t2 var
R3499:3503 subject_reduction <> gamma var
R3455:3464 type_derivation <> derivation ind
R3476:3479 type_derivation <> opty def
R3481:3481 subject_reduction <> o var
R3472:3473 subject_reduction <> t2 var
R3466:3470 subject_reduction <> gamma var
R3444:3446 Coq.Init.Logic <> :type_scope:x_'='_x not
R3443:3443 subject_reduction <> t var
R3447:3448 LamSF_Terms <> Op constr
R3450:3450 subject_reduction <> o var
R3404:3413 type_derivation <> derivation ind
R3423:3424 subject_reduction <> ty var
R3421:3421 subject_reduction <> t var
R3415:3419 subject_reduction <> gamma var
R3590:3600 type_derivation <> derive_inst constr
R3590:3600 type_derivation <> derive_inst constr
R3648:3658 type_derivation <> derive_gen1 constr
R3685:3688 type_derivation <> opty def
R3699:3702 LamSF_Terms <> lift def
R3707:3710 type_derivation <> opty def
R3699:3702 LamSF_Terms <> lift def
R3707:3710 type_derivation <> opty def
R3685:3688 type_derivation <> opty def
R3744:3771 type_derivation <> lift_rec_ty_preserves_derive thm
R3791:3802 type_derivation <> derive_push1 constr
R3791:3802 type_derivation <> derive_push1 constr
prf 3843:3855 <> derive_append
R3932:3941 type_derivation <> derivation ind
R3963:3964 subject_reduction <> ty var
R3961:3961 subject_reduction <> t var
R3949:3952 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R3944:3948 subject_reduction <> gamma var
R3953:3958 subject_reduction <> gamma2 var
R3918:3920 type_derivation <> wfc ind
R3922:3927 subject_reduction <> gamma2 var
R3878:3887 type_derivation <> derivation ind
R3897:3898 subject_reduction <> ty var
R3895:3895 subject_reduction <> t var
R3889:3893 subject_reduction <> gamma var
R4044:4052 type_derivation <> derive_op constr
R4064:4083 type_derivation <> append_preserves_wfc thm
R4117:4136 type_derivation <> append_preserves_wfc thm
R4157:4166 type_derivation <> derive_abs constr
R4187:4196 type_derivation <> derive_app constr
R4217:4227 type_derivation <> derive_inst constr
R4248:4258 type_derivation <> derive_gen1 constr
R4270:4276 Coq.Lists.List <> map_app thm
R4270:4276 Coq.Lists.List <> map_app thm
R4300:4303 LamSF_Terms <> lift def
R4314:4335 type_derivation <> lift_rec_preserves_wfc thm
R4357:4368 type_derivation <> derive_push1 constr
prf 4385:4394 <> derive_nil
R4461:4470 type_derivation <> derivation ind
R4480:4481 subject_reduction <> ty var
R4478:4478 subject_reduction <> t var
R4472:4476 subject_reduction <> gamma var
R4448:4450 type_derivation <> wfc ind
R4452:4456 subject_reduction <> gamma var
R4411:4420 type_derivation <> derivation ind
R4428:4429 subject_reduction <> ty var
R4426:4426 subject_reduction <> t var
R4422:4424 Coq.Init.Datatypes <> nil constr
R4526:4529 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R4523:4525 Coq.Init.Datatypes <> nil constr
R4526:4529 Coq.Init.Datatypes <> :list_scope:x_'++'_x not
R4523:4525 Coq.Init.Datatypes <> nil constr
R4554:4566 subject_reduction <> derive_append thm
prf 4587:4616 <> reduction_preserves_derivation
R4695:4704 type_derivation <> derivation ind
R4715:4716 subject_reduction <> ty var
R4712:4713 subject_reduction <> t1 var
R4706:4710 subject_reduction <> gamma var
R4676:4685 LamSF_reduction <> lamSF_red1 ind
R4689:4690 subject_reduction <> t1 var
R4687:4687 subject_reduction <> t var
R4640:4649 type_derivation <> derivation ind
R4659:4660 subject_reduction <> ty var
R4657:4657 subject_reduction <> t var
R4651:4655 subject_reduction <> gamma var
R4743:4743 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4990:4996 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5118:5118 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4967:4976 type_derivation <> derivation ind
R4987:4988 subject_reduction <> ty var
R4984:4985 subject_reduction <> t1 var
R4978:4982 subject_reduction <> gamma var
R4948:4957 LamSF_reduction <> lamSF_red1 ind
R4961:4962 subject_reduction <> t1 var
R4959:4959 subject_reduction <> t var
R4892:4901 type_derivation <> derivation ind
R4911:4912 subject_reduction <> ty var
R4909:4909 subject_reduction <> t var
R4903:4907 subject_reduction <> gamma var
R4841:4854 type_derivation_rwf <> derivation_rwf ind
R4865:4866 subject_reduction <> ty var
R4862:4863 subject_reduction <> t1 var
R4856:4860 subject_reduction <> gamma var
R4822:4831 LamSF_reduction <> lamSF_red1 ind
R4835:4836 subject_reduction <> t1 var
R4833:4833 subject_reduction <> t var
R4762:4775 type_derivation_rwf <> derivation_rwf ind
R4785:4786 subject_reduction <> ty var
R4783:4783 subject_reduction <> t var
R4777:4781 subject_reduction <> gamma var
R5092:5105 type_derivation_rwf <> derivation_rwf ind
R5116:5117 subject_reduction <> ty var
R5113:5114 subject_reduction <> t1 var
R5107:5111 subject_reduction <> gamma var
R5073:5082 LamSF_reduction <> lamSF_red1 ind
R5086:5087 subject_reduction <> t1 var
R5084:5084 subject_reduction <> t var
R5014:5027 type_derivation_rwf <> derivation_rwf ind
R5037:5038 subject_reduction <> ty var
R5035:5035 subject_reduction <> t var
R5029:5033 subject_reduction <> gamma var
R4743:4743 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4990:4996 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5118:5118 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4967:4976 type_derivation <> derivation ind
R4987:4988 subject_reduction <> ty var
R4984:4985 subject_reduction <> t1 var
R4978:4982 subject_reduction <> gamma var
R4948:4957 LamSF_reduction <> lamSF_red1 ind
R4961:4962 subject_reduction <> t1 var
R4959:4959 subject_reduction <> t var
R4892:4901 type_derivation <> derivation ind
R4911:4912 subject_reduction <> ty var
R4909:4909 subject_reduction <> t var
R4903:4907 subject_reduction <> gamma var
R4841:4854 type_derivation_rwf <> derivation_rwf ind
R4865:4866 subject_reduction <> ty var
R4862:4863 subject_reduction <> t1 var
R4856:4860 subject_reduction <> gamma var
R4822:4831 LamSF_reduction <> lamSF_red1 ind
R4835:4836 subject_reduction <> t1 var
R4833:4833 subject_reduction <> t var
R4762:4775 type_derivation_rwf <> derivation_rwf ind
R4785:4786 subject_reduction <> ty var
R4783:4783 subject_reduction <> t var
R4777:4781 subject_reduction <> gamma var
R5092:5105 type_derivation_rwf <> derivation_rwf ind
R5116:5117 subject_reduction <> ty var
R5113:5114 subject_reduction <> t1 var
R5107:5111 subject_reduction <> gamma var
R5073:5082 LamSF_reduction <> lamSF_red1 ind
R5086:5087 subject_reduction <> t1 var
R5084:5084 subject_reduction <> t var
R5014:5027 type_derivation_rwf <> derivation_rwf ind
R5037:5038 subject_reduction <> ty var
R5035:5035 subject_reduction <> t var
R5029:5033 subject_reduction <> gamma var
R5228:5241 type_derivation_rwf <> derivation_rwf ind
R5280:5282 Coq.Init.Datatypes <> snd def
R5285:5288 type_derivation_rwf <> pull def
R5244:5246 Coq.Lists.List <> map def
R5249:5252 LamSF_Terms <> lift def
R5254:5256 Coq.Init.Datatypes <> fst def
R5259:5262 type_derivation_rwf <> pull def
R5228:5241 type_derivation_rwf <> derivation_rwf ind
R5280:5282 Coq.Init.Datatypes <> snd def
R5285:5288 type_derivation_rwf <> pull def
R5244:5246 Coq.Lists.List <> map def
R5249:5252 LamSF_Terms <> lift def
R5254:5256 Coq.Init.Datatypes <> fst def
R5259:5262 type_derivation_rwf <> pull def
R5306:5321 type_derivation_rwf <> resi_implies_rwf thm
R5333:5366 type_derivation_resi <> derivation_implies_derivation_resi thm
R5378:5396 type_derivation <> derive_implies_wfcs thm
R5409:5419 type_derivation_rwf <> derive_pull thm
R5431:5448 type_derivation_rwf <> rwf_implies_derive thm
R5459:5477 type_derivation <> derive_implies_wfcs thm
R5607:5613 type_derivation_rwf <> rwf_abs constr
R5697:5703 type_derivation_rwf <> rwf_app constr
R5757:5763 type_derivation_rwf <> rwf_app constr
R5874:5909 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R5919:5923 LamSF_Terms <> subst def
R5946:5952 type_derivation <> removen def
R5960:5963 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R5946:5952 type_derivation <> removen def
R5960:5963 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R5990:6015 type_derivation <> subst_rec_preserves_derive thm
R6026:6043 type_derivation_rwf <> rwf_implies_derive thm
R6074:6087 type_derivation_rwf <> rwf_implies_wf thm
R6173:6183 operator_types <> instance_S2 thm
R6187:6191 type_derivation <> funty def
R6198:6202 type_derivation <> funty def
R6209:6213 type_derivation <> funty def
R6173:6183 operator_types <> instance_S2 thm
R6187:6191 type_derivation <> funty def
R6198:6202 type_derivation <> funty def
R6209:6213 type_derivation <> funty def
R6276:6282 type_derivation_rwf <> rwf_app constr
R6276:6282 type_derivation_rwf <> rwf_app constr
R6276:6282 type_derivation_rwf <> rwf_app constr
R6276:6282 type_derivation_rwf <> rwf_app constr
R6294:6298 type_derivation <> funty def
R6311:6312 type_derivation <> wf ind
R6331:6366 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R6377:6391 type_derivation <> derive_instance thm
R6377:6391 type_derivation <> derive_instance thm
R6414:6427 LamSF_Tactics <> transitive_red thm
R6414:6427 LamSF_Tactics <> transitive_red thm
R6450:6463 LamSF_Tactics <> transitive_red thm
R6450:6463 LamSF_Tactics <> transitive_red thm
R6474:6498 type_derivation <> preserves_contra_instance thm
R6474:6498 type_derivation <> preserves_contra_instance thm
R6509:6517 type_derivation <> wfs_funty constr
R6528:6530 type_derivation <> wfs ind
R6534:6536 LamSF_Terms <> App constr
R6539:6541 LamSF_Terms <> App constr
R6543:6546 Components <> s_op def
R6528:6530 type_derivation <> wfs ind
R6534:6536 LamSF_Terms <> App constr
R6539:6541 LamSF_Terms <> App constr
R6543:6546 Components <> s_op def
R6567:6586 type_derivation <> instance_implies_wfs thm
R6567:6586 type_derivation <> instance_implies_wfs thm
R6625:6644 type_derivation <> instance_implies_wfs thm
R6625:6644 type_derivation <> instance_implies_wfs thm
R6662:6675 type_derivation <> wf_implies_wfs thm
R6698:6723 type_derivation <> preserves_funty_r_instance thm
R6698:6723 type_derivation <> preserves_funty_r_instance thm
R6740:6765 type_derivation <> preserves_funty_r_instance thm
R6740:6765 type_derivation <> preserves_funty_r_instance thm
R6776:6778 type_derivation <> wfs ind
R6782:6784 LamSF_Terms <> App constr
R6787:6789 LamSF_Terms <> App constr
R6791:6794 Components <> s_op def
R6776:6778 type_derivation <> wfs ind
R6782:6784 LamSF_Terms <> App constr
R6787:6789 LamSF_Terms <> App constr
R6791:6794 Components <> s_op def
R6815:6834 type_derivation <> instance_implies_wfs thm
R6815:6834 type_derivation <> instance_implies_wfs thm
R6879:6886 type_derivation <> wf_funty constr
R6898:6905 type_derivation <> wf_funty constr
R6916:6918 type_derivation <> wfs ind
R6922:6924 LamSF_Terms <> App constr
R6927:6929 LamSF_Terms <> App constr
R6931:6934 Components <> s_op def
R6916:6918 type_derivation <> wfs ind
R6922:6924 LamSF_Terms <> App constr
R6927:6929 LamSF_Terms <> App constr
R6931:6934 Components <> s_op def
R6955:6974 type_derivation <> instance_implies_wfs thm
R6955:6974 type_derivation <> instance_implies_wfs thm
R7011:7020 type_derivation <> derive_app constr
R7030:7044 type_derivation <> derive_instance thm
R7030:7044 type_derivation <> derive_instance thm
R7066:7079 LamSF_Tactics <> transitive_red thm
R7066:7079 LamSF_Tactics <> transitive_red thm
R7103:7127 type_derivation <> preserves_contra_instance thm
R7138:7140 type_derivation <> wfs ind
R7144:7146 LamSF_Terms <> App constr
R7149:7151 LamSF_Terms <> App constr
R7153:7156 Components <> s_op def
R7138:7140 type_derivation <> wfs ind
R7144:7146 LamSF_Terms <> App constr
R7149:7151 LamSF_Terms <> App constr
R7153:7156 Components <> s_op def
R7177:7196 type_derivation <> instance_implies_wfs thm
R7177:7196 type_derivation <> instance_implies_wfs thm
R7363:7373 operator_types <> instance_A2 thm
R7377:7381 type_derivation <> funty def
R7388:7392 type_derivation <> funty def
R7399:7403 type_derivation <> funty def
R7363:7373 operator_types <> instance_A2 thm
R7377:7381 type_derivation <> funty def
R7388:7392 type_derivation <> funty def
R7399:7403 type_derivation <> funty def
R7466:7472 type_derivation_rwf <> rwf_app constr
R7466:7472 type_derivation_rwf <> rwf_app constr
R7466:7472 type_derivation_rwf <> rwf_app constr
R7484:7488 type_derivation <> funty def
R7501:7502 type_derivation <> wf ind
R7521:7556 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R7567:7581 type_derivation <> derive_instance thm
R7567:7581 type_derivation <> derive_instance thm
R7604:7617 LamSF_Tactics <> transitive_red thm
R7604:7617 LamSF_Tactics <> transitive_red thm
R7647:7654 type_derivation <> wf_funty constr
R7666:7673 type_derivation <> wf_funty constr
R7736:7746 operator_types <> instance_K2 thm
R7749:7753 type_derivation <> funty def
R7760:7764 type_derivation <> funty def
R7736:7746 operator_types <> instance_K2 thm
R7749:7753 type_derivation <> funty def
R7760:7764 type_derivation <> funty def
R7818:7822 type_derivation <> funty def
R7835:7836 type_derivation <> wf ind
R7855:7890 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R7901:7915 type_derivation <> derive_instance thm
R7901:7915 type_derivation <> derive_instance thm
R7999:8009 operator_types <> instance_E2 thm
R8012:8016 type_derivation <> funty def
R8023:8027 type_derivation <> funty def
R7999:8009 operator_types <> instance_E2 thm
R8012:8016 type_derivation <> funty def
R8023:8027 type_derivation <> funty def
R8091:8096 type_derivation_rwf <> rwf_op constr
R8107:8120 LamSF_Tactics <> transitive_red thm
R8107:8120 LamSF_Tactics <> transitive_red thm
R8131:8140 operator_types <> instance_K thm
R8131:8140 operator_types <> instance_K thm
R8154:8177 type_derivation <> preserves_funty_instance thm
R8154:8177 type_derivation <> preserves_funty_instance thm
R8191:8198 LamSF_Tactics <> zero_red constr
R8191:8198 LamSF_Tactics <> zero_red constr
R8240:8247 type_derivation <> wf_funty constr
R8258:8265 type_derivation <> wf_funty constr
R8415:8425 operator_types <> instance_E2 thm
R8428:8432 type_derivation <> funty def
R8439:8443 type_derivation <> funty def
R8415:8425 operator_types <> instance_E2 thm
R8428:8432 type_derivation <> funty def
R8439:8443 type_derivation <> funty def
R8506:8512 type_derivation_rwf <> rwf_app constr
R8506:8512 type_derivation_rwf <> rwf_app constr
R8527:8534 operator_types <> derive_I thm
R8527:8534 operator_types <> derive_I thm
R8556:8561 type_derivation_rwf <> rwf_op constr
R8572:8585 LamSF_Tactics <> transitive_red thm
R8572:8585 LamSF_Tactics <> transitive_red thm
R8599:8623 type_derivation <> preserves_contra_instance thm
R8637:8661 type_derivation <> preserves_contra_instance thm
R8673:8682 operator_types <> instance_K thm
R8694:8701 type_derivation <> wf_funty constr
R8712:8719 type_derivation <> wf_funty constr
R8730:8737 type_derivation <> wf_funty constr
R8886:8896 operator_types <> instance_E2 thm
R8899:8903 type_derivation <> funty def
R8886:8896 operator_types <> instance_E2 thm
R8899:8903 type_derivation <> funty def
R8964:8970 type_derivation_rwf <> rwf_app constr
R8964:8970 type_derivation_rwf <> rwf_app constr
R8984:8992 operator_types <> derive_KI thm
R8984:8992 operator_types <> derive_KI thm
R9010:9015 type_derivation_rwf <> rwf_op constr
R9010:9015 type_derivation_rwf <> rwf_op constr
R9048:9061 LamSF_Tactics <> transitive_red thm
R9048:9061 LamSF_Tactics <> transitive_red thm
R9071:9080 operator_types <> instance_K thm
R9071:9080 operator_types <> instance_K thm
R9100:9104 type_derivation <> funty def
R9110:9114 type_derivation <> funty def
R9146:9171 type_derivation <> preserves_funty_r_instance thm
R9146:9171 type_derivation <> preserves_funty_r_instance thm
R9200:9225 type_derivation <> preserves_funty_r_instance thm
R9244:9267 type_derivation <> preserves_funty_instance thm
R9279:9303 type_derivation <> preserves_contra_instance thm
R9472:9482 operator_types <> instance_G2 thm
R9485:9489 type_derivation <> funty def
R9496:9500 type_derivation <> funty def
R9472:9482 operator_types <> instance_G2 thm
R9485:9489 type_derivation <> funty def
R9496:9500 type_derivation <> funty def
R9554:9556 type_derivation <> wfs ind
R9554:9556 type_derivation <> wfs ind
R9573:9591 type_derivation <> derive_implies_wfcs thm
R9602:9611 type_derivation <> derivation ind
R9651:9654 LamSF_Terms <> lift def
R9656:9658 Coq.Init.Datatypes <> fst def
R9661:9664 type_derivation_rwf <> pull def
R9614:9616 Coq.Lists.List <> map def
R9619:9622 LamSF_Terms <> lift def
R9625:9627 Coq.Init.Datatypes <> fst def
R9630:9633 type_derivation_rwf <> pull def
R9602:9611 type_derivation <> derivation ind
R9651:9654 LamSF_Terms <> lift def
R9656:9658 Coq.Init.Datatypes <> fst def
R9661:9664 type_derivation_rwf <> pull def
R9614:9616 Coq.Lists.List <> map def
R9619:9622 LamSF_Terms <> lift def
R9625:9627 Coq.Init.Datatypes <> fst def
R9630:9633 type_derivation_rwf <> pull def
R9684:9687 LamSF_Terms <> lift def
R9698:9725 type_derivation <> lift_rec_ty_preserves_derive thm
R9736:9745 type_derivation <> derivation ind
R9785:9787 Coq.Init.Datatypes <> snd def
R9790:9793 type_derivation_rwf <> pull def
R9748:9750 Coq.Lists.List <> map def
R9753:9756 LamSF_Terms <> lift def
R9759:9761 Coq.Init.Datatypes <> fst def
R9764:9767 type_derivation_rwf <> pull def
R9736:9745 type_derivation <> derivation ind
R9785:9787 Coq.Init.Datatypes <> snd def
R9790:9793 type_derivation_rwf <> pull def
R9748:9750 Coq.Lists.List <> map def
R9753:9756 LamSF_Terms <> lift def
R9759:9761 Coq.Init.Datatypes <> fst def
R9764:9767 type_derivation_rwf <> pull def
R9810:9824 type_derivation <> derive_instance thm
R9835:9847 type_derivation_rwf <> instance_pull thm
R9858:9864 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R9868:9869 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R9939:9955 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9870:9879 type_derivation <> derivation ind
R9936:9938 subject_reduction <> ty0 var
R9917:9931 Components <> right_component def
R9882:9884 Coq.Lists.List <> map def
R9887:9890 LamSF_Terms <> lift def
R9893:9895 Coq.Init.Datatypes <> fst def
R9898:9901 type_derivation_rwf <> pull def
R9956:9965 type_derivation <> derivation ind
R10022:10026 type_derivation <> funty def
R10033:10035 Coq.Init.Datatypes <> snd def
R10037:10040 type_derivation_rwf <> pull def
R10028:10030 subject_reduction <> ty0 var
R10003:10016 Components <> left_component def
R9968:9970 Coq.Lists.List <> map def
R9973:9976 LamSF_Terms <> lift def
R9979:9981 Coq.Init.Datatypes <> fst def
R9984:9987 type_derivation_rwf <> pull def
R9858:9864 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R9868:9869 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R9939:9955 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9870:9879 type_derivation <> derivation ind
R9936:9938 subject_reduction <> ty0 var
R9917:9931 Components <> right_component def
R9882:9884 Coq.Lists.List <> map def
R9887:9890 LamSF_Terms <> lift def
R9893:9895 Coq.Init.Datatypes <> fst def
R9898:9901 type_derivation_rwf <> pull def
R9956:9965 type_derivation <> derivation ind
R10022:10026 type_derivation <> funty def
R10033:10035 Coq.Init.Datatypes <> snd def
R10037:10040 type_derivation_rwf <> pull def
R10028:10030 subject_reduction <> ty0 var
R10003:10016 Components <> left_component def
R9968:9970 Coq.Lists.List <> map def
R9973:9976 LamSF_Terms <> lift def
R9979:9981 Coq.Init.Datatypes <> fst def
R9984:9987 type_derivation_rwf <> pull def
R10058:10073 operator_types <> derive_compounds thm
R10085:10091 type_derivation_rwf <> pull_wf thm
R10115:10124 type_derivation <> derivation ind
R10193:10197 type_derivation <> funty def
R10249:10251 Coq.Init.Datatypes <> snd def
R10254:10257 type_derivation_rwf <> pull def
R10200:10203 LamSF_Terms <> lift def
R10221:10225 type_derivation <> quant def
R10228:10230 Coq.Init.Datatypes <> fst def
R10233:10236 type_derivation_rwf <> pull def
R10205:10207 Coq.Init.Datatypes <> fst def
R10210:10213 type_derivation_rwf <> pull def
R10174:10187 Components <> left_component def
R10128:10130 Coq.Lists.List <> map def
R10133:10136 LamSF_Terms <> lift def
R10139:10141 Coq.Init.Datatypes <> fst def
R10144:10147 type_derivation_rwf <> pull def
R10115:10124 type_derivation <> derivation ind
R10193:10197 type_derivation <> funty def
R10249:10251 Coq.Init.Datatypes <> snd def
R10254:10257 type_derivation_rwf <> pull def
R10200:10203 LamSF_Terms <> lift def
R10221:10225 type_derivation <> quant def
R10228:10230 Coq.Init.Datatypes <> fst def
R10233:10236 type_derivation_rwf <> pull def
R10205:10207 Coq.Init.Datatypes <> fst def
R10210:10213 type_derivation_rwf <> pull def
R10174:10187 Components <> left_component def
R10128:10130 Coq.Lists.List <> map def
R10133:10136 LamSF_Terms <> lift def
R10139:10141 Coq.Init.Datatypes <> fst def
R10144:10147 type_derivation_rwf <> pull def
R10276:10290 type_derivation <> derive_instance thm
R10302:10326 type_derivation <> preserves_contra_instance thm
R10337:10354 type_derivation_rwf <> pull_preserves_wfs thm
R10366:10385 type_derivation_rwf <> instance_quant_lift2 thm
R10397:10415 type_derivation <> derive_implies_wfcs thm
R10426:10435 type_derivation <> derivation ind
R10463:10467 type_derivation <> quant def
R10486:10490 type_derivation <> funty def
R10556:10558 Coq.Init.Datatypes <> snd def
R10561:10564 type_derivation_rwf <> pull def
R10493:10496 LamSF_Terms <> lift def
R10515:10519 type_derivation <> quant def
R10522:10524 Coq.Init.Datatypes <> fst def
R10527:10530 type_derivation_rwf <> pull def
R10499:10501 Coq.Init.Datatypes <> fst def
R10504:10507 type_derivation_rwf <> pull def
R10470:10472 Coq.Init.Datatypes <> fst def
R10475:10478 type_derivation_rwf <> pull def
R10444:10457 Components <> left_component def
R10426:10435 type_derivation <> derivation ind
R10463:10467 type_derivation <> quant def
R10486:10490 type_derivation <> funty def
R10556:10558 Coq.Init.Datatypes <> snd def
R10561:10564 type_derivation_rwf <> pull def
R10493:10496 LamSF_Terms <> lift def
R10515:10519 type_derivation <> quant def
R10522:10524 Coq.Init.Datatypes <> fst def
R10527:10530 type_derivation_rwf <> pull def
R10499:10501 Coq.Init.Datatypes <> fst def
R10504:10507 type_derivation_rwf <> pull def
R10470:10472 Coq.Init.Datatypes <> fst def
R10475:10478 type_derivation_rwf <> pull def
R10444:10457 Components <> left_component def
R10586:10595 type_derivation <> derive_gen thm
R10606:10615 type_derivation <> derivation ind
R10643:10647 type_derivation <> funty def
R10677:10681 type_derivation <> quant def
R10714:10716 Coq.Init.Datatypes <> snd def
R10719:10722 type_derivation_rwf <> pull def
R10684:10686 Coq.Init.Datatypes <> fst def
R10689:10692 type_derivation_rwf <> pull def
R10650:10654 type_derivation <> quant def
R10657:10659 Coq.Init.Datatypes <> fst def
R10662:10665 type_derivation_rwf <> pull def
R10624:10637 Components <> left_component def
R10606:10615 type_derivation <> derivation ind
R10643:10647 type_derivation <> funty def
R10677:10681 type_derivation <> quant def
R10714:10716 Coq.Init.Datatypes <> snd def
R10719:10722 type_derivation_rwf <> pull def
R10684:10686 Coq.Init.Datatypes <> fst def
R10689:10692 type_derivation_rwf <> pull def
R10650:10654 type_derivation <> quant def
R10657:10659 Coq.Init.Datatypes <> fst def
R10662:10665 type_derivation_rwf <> pull def
R10624:10637 Components <> left_component def
R10743:10753 type_derivation <> derive_push thm
R10764:10773 type_derivation <> push_quant thm
R10785:10803 type_derivation <> quant_preserves_wfs thm
R10814:10832 type_derivation <> derive_implies_wfcs thm
R10844:10861 type_derivation_rwf <> pull_preserves_wfs thm
R10872:10881 type_derivation <> derivation ind
R10909:10913 type_derivation <> funty def
R10916:10920 type_derivation <> quant def
R10923:10925 Coq.Init.Datatypes <> fst def
R10928:10931 type_derivation_rwf <> pull def
R10890:10903 Components <> left_component def
R10872:10881 type_derivation <> derivation ind
R10909:10913 type_derivation <> funty def
R10916:10920 type_derivation <> quant def
R10923:10925 Coq.Init.Datatypes <> fst def
R10928:10931 type_derivation_rwf <> pull def
R10890:10903 Components <> left_component def
R10957:10967 type_derivation <> derive_push thm
R10979:11000 type_derivation <> preserves_funty_r_push thm
R11013:11031 type_derivation <> quant_preserves_wfs thm
R11042:11060 type_derivation <> derive_implies_wfcs thm
R11072:11081 type_derivation_rwf <> quant_pull thm
R11093:11099 type_derivation_rwf <> rwf_app constr
R11111:11117 type_derivation_rwf <> rwf_app constr
R11129:11164 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R11175:11189 type_derivation <> derive_instance thm
R11175:11189 type_derivation <> derive_instance thm
R11212:11225 LamSF_Tactics <> transitive_red thm
R11212:11225 LamSF_Tactics <> transitive_red thm
R11247:11254 LamSF_Tactics <> succ_red constr
R11247:11254 LamSF_Tactics <> succ_red constr
R11265:11277 type_derivation <> instance_rule constr
R11265:11277 type_derivation <> instance_rule constr
R11318:11321 LamSF_Terms <> lift def
R11299:11307 type_derivation <> wfs_funty constr
R11299:11307 type_derivation <> wfs_funty constr
R11299:11307 type_derivation <> wfs_funty constr
R11299:11307 type_derivation <> wfs_funty constr
R11299:11307 type_derivation <> wfs_funty constr
R11332:11353 type_derivation <> lift_rec_preserves_wfs thm
R11332:11353 type_derivation <> lift_rec_preserves_wfs thm
R11368:11372 LamSF_Terms <> subst def
R11406:11418 LamSF_Substitution_term <> lift_rec_null thm
R11430:11447 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11469:11481 LamSF_Substitution_term <> lift_rec_null thm
R11406:11418 LamSF_Substitution_term <> lift_rec_null thm
R11430:11447 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11469:11481 LamSF_Substitution_term <> lift_rec_null thm
R11500:11525 type_derivation <> preserves_funty_r_instance thm
R11500:11525 type_derivation <> preserves_funty_r_instance thm
R11500:11525 type_derivation <> preserves_funty_r_instance thm
R11500:11525 type_derivation <> preserves_funty_r_instance thm
R11500:11525 type_derivation <> preserves_funty_r_instance thm
R11538:11556 type_derivation <> quant_preserves_wfs thm
R11568:11586 type_derivation <> derive_implies_wfcs thm
R11627:11640 type_derivation <> wf_implies_wfs thm
R11652:11660 type_derivation <> wfs_funty constr
R11672:11690 type_derivation <> quant_preserves_wfs thm
R11702:11720 type_derivation <> derive_implies_wfcs thm
R11732:11750 type_derivation <> quant_preserves_wfs thm
R11762:11780 type_derivation <> derive_implies_wfcs thm
R11792:11809 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11792:11809 LamSF_Substitution_term <> subst_rec_lift_rec thm
R11832:11844 LamSF_Substitution_term <> lift_rec_null thm
R11832:11844 LamSF_Substitution_term <> lift_rec_null thm
R11855:11862 LamSF_Tactics <> zero_red constr
R11882:11889 type_derivation <> wf_funty constr
R11882:11889 type_derivation <> wf_funty constr
R11882:11889 type_derivation <> wf_funty constr
R11882:11889 type_derivation <> wf_funty constr
R11882:11889 type_derivation <> wf_funty constr
R11910:11918 type_derivation <> wfs_funty constr
R11910:11918 type_derivation <> wfs_funty constr
R11931:11949 type_derivation <> quant_preserves_wfs thm
R11961:11979 type_derivation <> derive_implies_wfcs thm
R11991:12009 type_derivation <> quant_preserves_wfs thm
R12021:12039 type_derivation <> derive_implies_wfcs thm
R12087:12096 type_derivation <> derive_gen thm
R12163:12173 operator_types <> instance_Q2 thm
R12176:12180 type_derivation <> funty def
R12187:12191 type_derivation <> funty def
R12198:12202 type_derivation <> funty def
R12163:12173 operator_types <> instance_Q2 thm
R12176:12180 type_derivation <> funty def
R12187:12191 type_derivation <> funty def
R12198:12202 type_derivation <> funty def
R12265:12271 type_derivation_rwf <> rwf_app constr
R12265:12271 type_derivation_rwf <> rwf_app constr
R12283:12287 type_derivation <> funty def
R12300:12301 type_derivation <> wf ind
R12320:12355 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R12366:12380 type_derivation <> derive_instance thm
R12366:12380 type_derivation <> derive_instance thm
R12403:12416 LamSF_Tactics <> transitive_red thm
R12403:12416 LamSF_Tactics <> transitive_red thm
R12437:12444 LamSF_Tactics <> succ_red constr
R12437:12444 LamSF_Tactics <> succ_red constr
R12455:12467 type_derivation <> instance_rule constr
R12455:12467 type_derivation <> instance_rule constr
R12500:12518 type_derivation <> derive_implies_wfcs thm
R12540:12561 type_derivation <> lift_rec_preserves_wfs thm
R12540:12561 type_derivation <> lift_rec_preserves_wfs thm
R12572:12574 type_derivation <> wfs ind
R12577:12579 LamSF_Terms <> App constr
R12596:12598 LamSF_Terms <> App constr
R12601:12603 LamSF_Terms <> App constr
R12605:12608 Components <> s_op def
R12582:12584 LamSF_Terms <> App constr
R12586:12589 Components <> s_op def
R12572:12574 type_derivation <> wfs ind
R12577:12579 LamSF_Terms <> App constr
R12596:12598 LamSF_Terms <> App constr
R12601:12603 LamSF_Terms <> App constr
R12605:12608 Components <> s_op def
R12582:12584 LamSF_Terms <> App constr
R12586:12589 Components <> s_op def
R12631:12650 type_derivation <> instance_implies_wfs thm
R12631:12650 type_derivation <> instance_implies_wfs thm
R12666:12684 type_derivation <> derive_implies_wfcs thm
R12731:12735 LamSF_Terms <> subst def
R12777:12794 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12777:12794 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12777:12794 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12777:12794 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12777:12794 LamSF_Substitution_term <> subst_rec_lift_rec thm
R12824:12836 LamSF_Substitution_term <> lift_rec_null thm
R12824:12836 LamSF_Substitution_term <> lift_rec_null thm
R12824:12836 LamSF_Substitution_term <> lift_rec_null thm
R12824:12836 LamSF_Substitution_term <> lift_rec_null thm
R12848:12871 type_derivation <> preserves_funty_instance thm
R12882:12900 type_derivation <> derive_implies_wfcs thm
R12911:12913 type_derivation <> wfs ind
R12916:12918 LamSF_Terms <> App constr
R12935:12937 LamSF_Terms <> App constr
R12940:12942 LamSF_Terms <> App constr
R12944:12947 Components <> s_op def
R12921:12923 LamSF_Terms <> App constr
R12925:12928 Components <> s_op def
R12911:12913 type_derivation <> wfs ind
R12916:12918 LamSF_Terms <> App constr
R12935:12937 LamSF_Terms <> App constr
R12940:12942 LamSF_Terms <> App constr
R12944:12947 Components <> s_op def
R12921:12923 LamSF_Terms <> App constr
R12925:12928 Components <> s_op def
R12970:12989 type_derivation <> instance_implies_wfs thm
R12970:12989 type_derivation <> instance_implies_wfs thm
R13005:13023 type_derivation <> derive_implies_wfcs thm
R13056:13063 LamSF_Tactics <> zero_red constr
R13074:13081 type_derivation <> wf_funty constr
R13092:13110 type_derivation <> derive_implies_wfcs thm
R13121:13122 type_derivation <> wf ind
R13125:13127 LamSF_Terms <> App constr
R13130:13132 LamSF_Terms <> App constr
R13134:13137 Components <> s_op def
R13121:13122 type_derivation <> wf ind
R13125:13127 LamSF_Terms <> App constr
R13130:13132 LamSF_Terms <> App constr
R13134:13137 Components <> s_op def
R13159:13172 type_derivation_rwf <> rwf_implies_wf thm
R13225:13238 type_derivation_rwf <> rwf_implies_wf thm
R13333:13343 operator_types <> instance_Q2 thm
R13346:13350 type_derivation <> funty def
R13357:13361 type_derivation <> funty def
R13368:13372 type_derivation <> funty def
R13333:13343 operator_types <> instance_Q2 thm
R13346:13350 type_derivation <> funty def
R13357:13361 type_derivation <> funty def
R13368:13372 type_derivation <> funty def
R13427:13429 type_derivation <> wfs ind
R13433:13437 type_derivation <> funty def
R13443:13447 type_derivation <> funty def
R13427:13429 type_derivation <> wfs ind
R13433:13437 type_derivation <> funty def
R13443:13447 type_derivation <> funty def
R13469:13488 type_derivation <> instance_implies_wfs thm
R13469:13488 type_derivation <> instance_implies_wfs thm
R13503:13521 type_derivation <> derive_implies_wfcs thm
R13562:13564 type_derivation <> wfs ind
R13562:13564 type_derivation <> wfs ind
R13581:13599 type_derivation <> derive_implies_wfcs thm
R13610:13619 type_derivation <> derivation ind
R13659:13662 LamSF_Terms <> lift def
R13664:13666 Coq.Init.Datatypes <> fst def
R13669:13672 type_derivation_rwf <> pull def
R13622:13624 Coq.Lists.List <> map def
R13627:13630 LamSF_Terms <> lift def
R13633:13635 Coq.Init.Datatypes <> fst def
R13638:13641 type_derivation_rwf <> pull def
R13610:13619 type_derivation <> derivation ind
R13659:13662 LamSF_Terms <> lift def
R13664:13666 Coq.Init.Datatypes <> fst def
R13669:13672 type_derivation_rwf <> pull def
R13622:13624 Coq.Lists.List <> map def
R13627:13630 LamSF_Terms <> lift def
R13633:13635 Coq.Init.Datatypes <> fst def
R13638:13641 type_derivation_rwf <> pull def
R13692:13695 LamSF_Terms <> lift def
R13706:13733 type_derivation <> lift_rec_ty_preserves_derive thm
R13744:13753 type_derivation <> derivation ind
R13793:13795 Coq.Init.Datatypes <> snd def
R13798:13801 type_derivation_rwf <> pull def
R13756:13758 Coq.Lists.List <> map def
R13761:13764 LamSF_Terms <> lift def
R13767:13769 Coq.Init.Datatypes <> fst def
R13772:13775 type_derivation_rwf <> pull def
R13744:13753 type_derivation <> derivation ind
R13793:13795 Coq.Init.Datatypes <> snd def
R13798:13801 type_derivation_rwf <> pull def
R13756:13758 Coq.Lists.List <> map def
R13761:13764 LamSF_Terms <> lift def
R13767:13769 Coq.Init.Datatypes <> fst def
R13772:13775 type_derivation_rwf <> pull def
R13818:13832 type_derivation <> derive_instance thm
R13843:13855 type_derivation_rwf <> instance_pull thm
R13866:13872 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13876:13877 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13947:13963 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13878:13887 type_derivation <> derivation ind
R13944:13946 subject_reduction <> ty0 var
R13925:13939 Components <> right_component def
R13890:13892 Coq.Lists.List <> map def
R13895:13898 LamSF_Terms <> lift def
R13901:13903 Coq.Init.Datatypes <> fst def
R13906:13909 type_derivation_rwf <> pull def
R13964:13973 type_derivation <> derivation ind
R14030:14034 type_derivation <> funty def
R14041:14043 Coq.Init.Datatypes <> snd def
R14045:14048 type_derivation_rwf <> pull def
R14036:14038 subject_reduction <> ty0 var
R14011:14024 Components <> left_component def
R13976:13978 Coq.Lists.List <> map def
R13981:13984 LamSF_Terms <> lift def
R13987:13989 Coq.Init.Datatypes <> fst def
R13992:13995 type_derivation_rwf <> pull def
R13866:13872 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13876:13877 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R13947:13963 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13878:13887 type_derivation <> derivation ind
R13944:13946 subject_reduction <> ty0 var
R13925:13939 Components <> right_component def
R13890:13892 Coq.Lists.List <> map def
R13895:13898 LamSF_Terms <> lift def
R13901:13903 Coq.Init.Datatypes <> fst def
R13906:13909 type_derivation_rwf <> pull def
R13964:13973 type_derivation <> derivation ind
R14030:14034 type_derivation <> funty def
R14041:14043 Coq.Init.Datatypes <> snd def
R14045:14048 type_derivation_rwf <> pull def
R14036:14038 subject_reduction <> ty0 var
R14011:14024 Components <> left_component def
R13976:13978 Coq.Lists.List <> map def
R13981:13984 LamSF_Terms <> lift def
R13987:13989 Coq.Init.Datatypes <> fst def
R13992:13995 type_derivation_rwf <> pull def
R14066:14081 operator_types <> derive_compounds thm
R14093:14099 type_derivation_rwf <> pull_wf thm
R14123:14132 type_derivation <> derivation ind
R14201:14205 type_derivation <> funty def
R14257:14259 Coq.Init.Datatypes <> snd def
R14262:14265 type_derivation_rwf <> pull def
R14208:14211 LamSF_Terms <> lift def
R14229:14233 type_derivation <> quant def
R14236:14238 Coq.Init.Datatypes <> fst def
R14241:14244 type_derivation_rwf <> pull def
R14213:14215 Coq.Init.Datatypes <> fst def
R14218:14221 type_derivation_rwf <> pull def
R14182:14195 Components <> left_component def
R14136:14138 Coq.Lists.List <> map def
R14141:14144 LamSF_Terms <> lift def
R14147:14149 Coq.Init.Datatypes <> fst def
R14152:14155 type_derivation_rwf <> pull def
R14123:14132 type_derivation <> derivation ind
R14201:14205 type_derivation <> funty def
R14257:14259 Coq.Init.Datatypes <> snd def
R14262:14265 type_derivation_rwf <> pull def
R14208:14211 LamSF_Terms <> lift def
R14229:14233 type_derivation <> quant def
R14236:14238 Coq.Init.Datatypes <> fst def
R14241:14244 type_derivation_rwf <> pull def
R14213:14215 Coq.Init.Datatypes <> fst def
R14218:14221 type_derivation_rwf <> pull def
R14182:14195 Components <> left_component def
R14136:14138 Coq.Lists.List <> map def
R14141:14144 LamSF_Terms <> lift def
R14147:14149 Coq.Init.Datatypes <> fst def
R14152:14155 type_derivation_rwf <> pull def
R14284:14298 type_derivation <> derive_instance thm
R14310:14334 type_derivation <> preserves_contra_instance thm
R14345:14362 type_derivation_rwf <> pull_preserves_wfs thm
R14374:14393 type_derivation_rwf <> instance_quant_lift2 thm
R14405:14423 type_derivation <> derive_implies_wfcs thm
R14434:14443 type_derivation <> derivation ind
R14471:14475 type_derivation <> quant def
R14494:14498 type_derivation <> funty def
R14564:14566 Coq.Init.Datatypes <> snd def
R14569:14572 type_derivation_rwf <> pull def
R14501:14504 LamSF_Terms <> lift def
R14523:14527 type_derivation <> quant def
R14530:14532 Coq.Init.Datatypes <> fst def
R14535:14538 type_derivation_rwf <> pull def
R14507:14509 Coq.Init.Datatypes <> fst def
R14512:14515 type_derivation_rwf <> pull def
R14478:14480 Coq.Init.Datatypes <> fst def
R14483:14486 type_derivation_rwf <> pull def
R14452:14465 Components <> left_component def
R14434:14443 type_derivation <> derivation ind
R14471:14475 type_derivation <> quant def
R14494:14498 type_derivation <> funty def
R14564:14566 Coq.Init.Datatypes <> snd def
R14569:14572 type_derivation_rwf <> pull def
R14501:14504 LamSF_Terms <> lift def
R14523:14527 type_derivation <> quant def
R14530:14532 Coq.Init.Datatypes <> fst def
R14535:14538 type_derivation_rwf <> pull def
R14507:14509 Coq.Init.Datatypes <> fst def
R14512:14515 type_derivation_rwf <> pull def
R14478:14480 Coq.Init.Datatypes <> fst def
R14483:14486 type_derivation_rwf <> pull def
R14452:14465 Components <> left_component def
R14594:14603 type_derivation <> derive_gen thm
R14614:14623 type_derivation <> derivation ind
R14651:14655 type_derivation <> funty def
R14685:14689 type_derivation <> quant def
R14722:14724 Coq.Init.Datatypes <> snd def
R14727:14730 type_derivation_rwf <> pull def
R14692:14694 Coq.Init.Datatypes <> fst def
R14697:14700 type_derivation_rwf <> pull def
R14658:14662 type_derivation <> quant def
R14665:14667 Coq.Init.Datatypes <> fst def
R14670:14673 type_derivation_rwf <> pull def
R14632:14645 Components <> left_component def
R14614:14623 type_derivation <> derivation ind
R14651:14655 type_derivation <> funty def
R14685:14689 type_derivation <> quant def
R14722:14724 Coq.Init.Datatypes <> snd def
R14727:14730 type_derivation_rwf <> pull def
R14692:14694 Coq.Init.Datatypes <> fst def
R14697:14700 type_derivation_rwf <> pull def
R14658:14662 type_derivation <> quant def
R14665:14667 Coq.Init.Datatypes <> fst def
R14670:14673 type_derivation_rwf <> pull def
R14632:14645 Components <> left_component def
R14751:14761 type_derivation <> derive_push thm
R14772:14781 type_derivation <> push_quant thm
R14793:14811 type_derivation <> quant_preserves_wfs thm
R14822:14840 type_derivation <> derive_implies_wfcs thm
R14852:14869 type_derivation_rwf <> pull_preserves_wfs thm
R14880:14889 type_derivation <> derivation ind
R14917:14921 type_derivation <> funty def
R14924:14928 type_derivation <> quant def
R14931:14933 Coq.Init.Datatypes <> fst def
R14936:14939 type_derivation_rwf <> pull def
R14898:14911 Components <> left_component def
R14880:14889 type_derivation <> derivation ind
R14917:14921 type_derivation <> funty def
R14924:14928 type_derivation <> quant def
R14931:14933 Coq.Init.Datatypes <> fst def
R14936:14939 type_derivation_rwf <> pull def
R14898:14911 Components <> left_component def
R14965:14975 type_derivation <> derive_push thm
R14987:15008 type_derivation <> preserves_funty_r_push thm
R15021:15039 type_derivation <> quant_preserves_wfs thm
R15050:15068 type_derivation <> derive_implies_wfcs thm
R15080:15089 type_derivation_rwf <> quant_pull thm
R15101:15107 type_derivation_rwf <> rwf_app constr
R15119:15125 type_derivation_rwf <> rwf_app constr
R15137:15172 type_derivation_rwf <> derivation_implies_derivation_rwf_wf thm
R15183:15197 type_derivation <> derive_instance thm
R15183:15197 type_derivation <> derive_instance thm
R15220:15233 LamSF_Tactics <> transitive_red thm
R15220:15233 LamSF_Tactics <> transitive_red thm
R15256:15281 type_derivation <> preserves_funty_r_instance thm
R15256:15281 type_derivation <> preserves_funty_r_instance thm
R15292:15294 type_derivation <> wfs ind
R15298:15302 type_derivation <> funty def
R15308:15312 type_derivation <> funty def
R15292:15294 type_derivation <> wfs ind
R15298:15302 type_derivation <> funty def
R15308:15312 type_derivation <> funty def
R15349:15374 type_derivation <> preserves_funty_r_instance thm
R15396:15397 type_derivation <> wf ind
R15399:15403 type_derivation <> funty def
R15396:15397 type_derivation <> wf ind
R15399:15403 type_derivation <> funty def
R15422:15435 type_derivation_rwf <> rwf_implies_wf thm
R15468:15477 type_derivation <> derive_app constr
R15468:15477 type_derivation <> derive_app constr
R15499:15503 type_derivation <> funty def