-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathtype_derivation_rwf.glob
1158 lines (1158 loc) · 50.7 KB
/
type_derivation_rwf.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 ca39961d56635676ef09e6dee65174c5
Ftype_derivation_rwf
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
R2353:2364 LamSF_Closed <> <> lib
R2382:2396 type_derivation <> <> lib
R2414:2433 type_derivation_resi <> <> lib
ind 2494:2507 <> derivation_rwf
constr 2551:2556 <> rwf_op
constr 2696:2702 <> rwf_var
constr 2858:2865 <> rwf_weak
constr 3022:3028 <> rwf_abs
constr 3181:3187 <> rwf_app
R2531:2535 LamSF_Terms <> lamSF ind
R2522:2526 LamSF_Terms <> lamSF ind
R2511:2517 type_derivation <> context def
R2662:2675 type_derivation_rwf <> derivation_rwf ind
R2690:2691 type_derivation_rwf <> ty var
R2684:2685 LamSF_Terms <> Op constr
R2687:2687 type_derivation_rwf <> o var
R2677:2681 type_derivation_rwf <> gamma var
R2617:2618 type_derivation <> wf ind
R2620:2621 type_derivation_rwf <> ty var
R2604:2606 type_derivation <> wfc ind
R2608:2612 type_derivation_rwf <> gamma var
R2580:2587 type_derivation <> instance def
R2598:2599 type_derivation_rwf <> ty var
R2590:2593 type_derivation <> opty def
R2595:2595 type_derivation_rwf <> o var
R2812:2825 type_derivation_rwf <> derivation_rwf ind
R2852:2854 type_derivation_rwf <> ty2 var
R2845:2847 LamSF_Terms <> Ref constr
R2828:2831 Coq.Init.Datatypes <> cons constr
R2837:2841 type_derivation_rwf <> gamma var
R2833:2835 type_derivation_rwf <> ty1 var
R2759:2761 type_derivation <> wfc ind
R2763:2767 type_derivation_rwf <> gamma var
R2749:2750 type_derivation <> wf ind
R2752:2754 type_derivation_rwf <> ty2 var
R2729:2736 type_derivation <> instance def
R2742:2744 type_derivation_rwf <> ty2 var
R2738:2740 type_derivation_rwf <> ty1 var
R2973:2986 type_derivation_rwf <> derivation_rwf ind
R3017:3018 type_derivation_rwf <> ty var
R3006:3008 LamSF_Terms <> Ref constr
R3011:3011 Coq.Init.Datatypes <> S constr
R3013:3013 type_derivation_rwf <> i var
R2989:2992 Coq.Init.Datatypes <> cons constr
R2998:3002 type_derivation_rwf <> gamma var
R2994:2996 type_derivation_rwf <> ty1 var
R2928:2930 type_derivation <> wfs ind
R2932:2934 type_derivation_rwf <> ty1 var
R2893:2906 type_derivation_rwf <> derivation_rwf ind
R2922:2923 type_derivation_rwf <> ty var
R2915:2917 LamSF_Terms <> Ref constr
R2919:2919 type_derivation_rwf <> i var
R2908:2912 type_derivation_rwf <> gamma var
R3134:3147 type_derivation_rwf <> derivation_rwf ind
R3164:3168 type_derivation <> funty def
R3174:3176 type_derivation_rwf <> ty2 var
R3170:3172 type_derivation_rwf <> ty1 var
R3156:3158 LamSF_Terms <> Abs constr
R3160:3160 type_derivation_rwf <> t var
R3149:3153 type_derivation_rwf <> gamma var
R3076:3089 type_derivation_rwf <> derivation_rwf ind
R3110:3112 type_derivation_rwf <> ty2 var
R3108:3108 type_derivation_rwf <> t var
R3092:3095 Coq.Init.Datatypes <> cons constr
R3101:3105 type_derivation_rwf <> gamma var
R3097:3099 type_derivation_rwf <> ty1 var
R3370:3383 type_derivation_rwf <> derivation_rwf ind
R3401:3403 type_derivation_rwf <> ty2 var
R3392:3394 LamSF_Terms <> App constr
R3398:3398 type_derivation_rwf <> u var
R3396:3396 type_derivation_rwf <> t var
R3385:3389 type_derivation_rwf <> gamma var
R3293:3302 type_derivation <> derivation ind
R3312:3314 type_derivation_rwf <> ty1 var
R3310:3310 type_derivation_rwf <> u var
R3304:3308 type_derivation_rwf <> gamma var
R3234:3247 type_derivation_rwf <> derivation_rwf ind
R3258:3262 type_derivation <> funty def
R3268:3270 type_derivation_rwf <> ty2 var
R3264:3266 type_derivation_rwf <> ty1 var
R3255:3255 type_derivation_rwf <> t var
R3249:3253 type_derivation_rwf <> gamma var
R3424:3429 type_derivation_rwf <> rwf_op constr
R3431:3437 type_derivation_rwf <> rwf_var constr
R3439:3446 type_derivation_rwf <> rwf_weak constr
R3448:3454 type_derivation_rwf <> rwf_abs constr
R3456:3462 type_derivation_rwf <> rwf_app constr
prf 3500:3515 <> rwf_implies_resi
R3568:3582 type_derivation_resi <> derivation_resi ind
R3592:3593 type_derivation_rwf <> ty var
R3590:3590 type_derivation_rwf <> t var
R3584:3588 type_derivation_rwf <> gamma var
R3539:3552 type_derivation_rwf <> derivation_rwf ind
R3562:3563 type_derivation_rwf <> ty var
R3560:3560 type_derivation_rwf <> t var
R3554:3558 type_derivation_rwf <> gamma var
R3657:3664 type_derivation_resi <> resi_var constr
R3676:3695 type_derivation <> instance_implies_wfs thm
R3706:3719 type_derivation <> wf_implies_wfs thm
R3731:3738 type_derivation_resi <> resi_app constr
def 3759:3767 <> succ_left
R3776:3778 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
R3773:3775 Coq.Init.Datatypes <> nat ind
R3779:3783 LamSF_Terms <> lamSF ind
R3789:3789 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3799:3800 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3806:3806 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3790:3790 Coq.Init.Datatypes <> S constr
R3793:3795 Coq.Init.Datatypes <> fst def
R3797:3797 type_derivation_rwf <> p var
R3801:3803 Coq.Init.Datatypes <> snd def
R3805:3805 type_derivation_rwf <> p var
def 3820:3823 <> pull
R3838:3839 type_derivation_rwf <> ty var
R3849:3851 LamSF_Terms <> Abs constr
R3860:3868 type_derivation_rwf <> succ_left def
R3871:3874 type_derivation_rwf <> pull def
R3883:3885 LamSF_Terms <> App constr
R3888:3890 LamSF_Terms <> App constr
R3893:3894 LamSF_Terms <> Op constr
R3896:3898 LamSF_Terms <> Sop constr
R3913:3913 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3927:3947 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3997:3997 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R3914:3916 Coq.Init.Datatypes <> fst def
R3918:3921 type_derivation_rwf <> pull def
R3948:3952 type_derivation <> funty def
R3982:3984 Coq.Init.Datatypes <> snd def
R3987:3990 type_derivation_rwf <> pull def
R3955:3958 LamSF_Terms <> lift def
R3961:3963 Coq.Init.Datatypes <> fst def
R3965:3968 type_derivation_rwf <> pull def
R4006:4006 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4008:4008 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4011:4011 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4009:4010 type_derivation_rwf <> ty var
prf 4025:4047 <> lift_rec_preserves_pull
R4087:4105 Coq.Init.Logic <> :type_scope:x_'='_x not
R4066:4069 type_derivation_rwf <> pull def
R4071:4078 LamSF_Terms <> lift_rec def
R4085:4085 type_derivation_rwf <> k var
R4083:4083 type_derivation_rwf <> n var
R4080:4081 type_derivation_rwf <> ty var
R4106:4106 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4120:4121 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4165:4165 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R4107:4109 Coq.Init.Datatypes <> fst def
R4112:4115 type_derivation_rwf <> pull def
R4117:4118 type_derivation_rwf <> ty var
R4122:4129 LamSF_Terms <> lift_rec def
R4164:4164 type_derivation_rwf <> k var
R4160:4160 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4148:4150 Coq.Init.Datatypes <> fst def
R4152:4155 type_derivation_rwf <> pull def
R4157:4158 type_derivation_rwf <> ty var
R4161:4161 type_derivation_rwf <> n var
R4132:4134 Coq.Init.Datatypes <> snd def
R4137:4140 type_derivation_rwf <> pull def
R4142:4143 type_derivation_rwf <> ty var
R4236:4243 LamSF_Terms <> lift_rec def
R4251:4258 LamSF_Terms <> lift_rec def
R4251:4258 LamSF_Terms <> lift_rec def
R4268:4271 type_derivation_rwf <> pull def
R4279:4282 type_derivation_rwf <> pull def
R4279:4282 type_derivation_rwf <> pull def
R4318:4326 type_derivation_rwf <> succ_left def
R4357:4359 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4344:4346 Coq.Init.Datatypes <> fst def
R4349:4352 type_derivation_rwf <> pull def
R4360:4360 Coq.Init.Datatypes <> S constr
R4371:4371 Coq.Init.Datatypes <> S constr
R4387:4389 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4374:4376 Coq.Init.Datatypes <> fst def
R4379:4382 type_derivation_rwf <> pull def
R4371:4371 Coq.Init.Datatypes <> S constr
R4387:4389 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4374:4376 Coq.Init.Datatypes <> fst def
R4379:4382 type_derivation_rwf <> pull def
R4357:4359 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R4344:4346 Coq.Init.Datatypes <> fst def
R4349:4352 type_derivation_rwf <> pull def
R4360:4360 Coq.Init.Datatypes <> S constr
R4545:4548 LamSF_Terms <> lift def
R4592:4595 LamSF_Terms <> lift def
R4606:4618 LamSF_Substitution_term <> lift_lift_rec thm
R4606:4618 LamSF_Substitution_term <> lift_lift_rec thm
prf 4651:4668 <> pull_preserves_wfs
R4692:4694 type_derivation <> wfs ind
R4697:4699 Coq.Init.Datatypes <> snd def
R4702:4705 type_derivation_rwf <> pull def
R4707:4708 type_derivation_rwf <> ty var
R4682:4684 type_derivation <> wfs ind
R4686:4687 type_derivation_rwf <> ty var
R4767:4775 type_derivation <> wfs_funty constr
R4785:4788 LamSF_Terms <> lift def
R4799:4820 type_derivation <> lift_rec_preserves_wfs thm
prf 4837:4853 <> pull_reflects_wfs
R4890:4892 type_derivation <> wfs ind
R4894:4895 type_derivation_rwf <> ty var
R4867:4869 type_derivation <> wfs ind
R4872:4874 Coq.Init.Datatypes <> snd def
R4877:4880 type_derivation_rwf <> pull def
R4882:4883 type_derivation_rwf <> ty var
R5100:5108 type_derivation <> wfs_funty constr
R5118:5121 LamSF_Terms <> lift def
R5137:5157 type_derivation <> lift_rec_reflects_wfs thm
prf 5175:5184 <> quant_pull
R5210:5213 type_derivation <> push def
R5253:5254 type_derivation_rwf <> ty var
R5216:5220 type_derivation <> quant def
R5238:5240 Coq.Init.Datatypes <> snd def
R5242:5245 type_derivation_rwf <> pull def
R5247:5248 type_derivation_rwf <> ty var
R5223:5225 Coq.Init.Datatypes <> fst def
R5227:5230 type_derivation_rwf <> pull def
R5232:5233 type_derivation_rwf <> ty var
R5200:5202 type_derivation <> wfs ind
R5204:5205 type_derivation_rwf <> ty var
R5316:5323 LamSF_Tactics <> zero_red constr
R5316:5323 LamSF_Tactics <> zero_red constr
R5316:5323 LamSF_Tactics <> zero_red constr
R5316:5323 LamSF_Tactics <> zero_red constr
R5373:5396 LamSF_Tactics <> preserves_abs_multi_step thm
R5473:5486 LamSF_Tactics <> transitive_red thm
R5473:5486 LamSF_Tactics <> transitive_red thm
R5498:5507 type_derivation <> push_quant thm
R5518:5535 type_derivation_rwf <> pull_preserves_wfs thm
R5547:5568 type_derivation <> preserves_funty_r_push thm
prf 5584:5590 <> pull_wf
R5615:5616 type_derivation <> wf ind
R5619:5621 Coq.Init.Datatypes <> snd def
R5624:5627 type_derivation_rwf <> pull def
R5629:5630 type_derivation_rwf <> ty var
R5605:5607 type_derivation <> wfs ind
R5609:5610 type_derivation_rwf <> ty var
R5781:5788 type_derivation <> wf_funty constr
R5798:5801 LamSF_Terms <> lift def
R5812:5833 type_derivation <> lift_rec_preserves_wfs thm
prf 5849:5856 <> pull_wf2
R5886:5888 Coq.Init.Logic <> :type_scope:x_'='_x not
R5879:5882 type_derivation_rwf <> pull def
R5884:5885 type_derivation_rwf <> ty var
R5889:5889 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R5891:5891 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R5894:5894 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R5892:5893 type_derivation_rwf <> ty var
R5870:5871 type_derivation <> wf ind
R5873:5874 type_derivation_rwf <> ty var
R5935:5936 type_derivation <> wf ind
R5935:5936 type_derivation <> wf ind
R5988:5991 LamSF_Terms <> lift def
R6002:6014 LamSF_Substitution_term <> lift_rec_null thm
R6002:6014 LamSF_Substitution_term <> lift_rec_null thm
prf 6036:6045 <> pull_quant
R6079:6081 Coq.Init.Logic <> :type_scope:x_'='_x not
R6063:6066 type_derivation_rwf <> pull def
R6068:6072 type_derivation <> quant def
R6076:6077 type_derivation_rwf <> ty var
R6074:6074 type_derivation_rwf <> j var
R6082:6082 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R6100:6101 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R6115:6115 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R6084:6086 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R6083:6083 type_derivation_rwf <> j var
R6087:6089 Coq.Init.Datatypes <> fst def
R6092:6095 type_derivation_rwf <> pull def
R6097:6098 type_derivation_rwf <> ty var
R6102:6104 Coq.Init.Datatypes <> snd def
R6107:6110 type_derivation_rwf <> pull def
R6112:6113 type_derivation_rwf <> ty var
R6164:6167 type_derivation_rwf <> pull def
R6164:6167 type_derivation_rwf <> pull def
R6210:6218 type_derivation_rwf <> succ_left def
prf 6241:6249 <> pull_rank
R6291:6294 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R6273:6276 Components <> rank def
R6278:6280 Coq.Init.Datatypes <> snd def
R6282:6285 type_derivation_rwf <> pull def
R6287:6288 type_derivation_rwf <> ty var
R6295:6298 Components <> rank def
R6300:6301 type_derivation_rwf <> ty var
R6263:6265 type_derivation <> wfs ind
R6267:6268 type_derivation_rwf <> ty var
R6379:6383 type_derivation <> funty def
R6386:6389 Components <> s_op def
R6392:6395 type_derivation_rwf <> pull def
R6403:6406 type_derivation_rwf <> pull def
R6403:6406 type_derivation_rwf <> pull def
R6416:6419 Components <> rank def
R6427:6430 Components <> rank def
R6427:6430 Components <> rank def
R6448:6451 LamSF_Terms <> lift def
R6462:6484 Components <> lift_rec_preserves_rank thm
R6462:6484 Components <> lift_rec_preserves_rank thm
R6510:6514 type_derivation <> funty def
R6517:6520 Components <> s_op def
R6523:6526 type_derivation_rwf <> pull def
R6534:6537 type_derivation_rwf <> pull def
R6534:6537 type_derivation_rwf <> pull def
R6554:6557 type_derivation_rwf <> pull def
R6554:6557 type_derivation_rwf <> pull def
prf 6588:6596 <> pull_opty
R6623:6625 Coq.Init.Logic <> :type_scope:x_'='_x not
R6610:6613 type_derivation_rwf <> pull def
R6616:6619 type_derivation <> opty def
R6621:6621 type_derivation_rwf <> o var
R6626:6626 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R6635:6636 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R6648:6648 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R6627:6632 type_derivation <> op_abs def
R6634:6634 type_derivation_rwf <> o var
R6637:6645 type_derivation <> opty_core def
R6647:6647 type_derivation_rwf <> o var
prf 6696:6714 <> instance_quant_lift
R6741:6748 type_derivation <> instance def
R6771:6772 type_derivation_rwf <> ty var
R6750:6754 type_derivation <> quant def
R6759:6762 LamSF_Terms <> lift def
R6766:6767 type_derivation_rwf <> ty var
R6764:6764 type_derivation_rwf <> n var
R6756:6756 type_derivation_rwf <> n var
R6731:6733 type_derivation <> wfs ind
R6735:6736 type_derivation_rwf <> ty var
R6825:6828 LamSF_Terms <> lift def
R6839:6851 LamSF_Substitution_term <> lift_rec_null thm
R6839:6851 LamSF_Substitution_term <> lift_rec_null thm
R6862:6869 LamSF_Tactics <> zero_red constr
R6903:6907 LamSF_Terms <> subst def
R6918:6922 type_derivation <> quant def
R6927:6930 LamSF_Terms <> lift def
R6933:6933 Coq.Init.Datatypes <> S constr
R6910:6912 LamSF_Terms <> Ref constr
R6888:6895 LamSF_Tactics <> succ_red constr
R6903:6907 LamSF_Terms <> subst def
R6918:6922 type_derivation <> quant def
R6927:6930 LamSF_Terms <> lift def
R6933:6933 Coq.Init.Datatypes <> S constr
R6910:6912 LamSF_Terms <> Ref constr
R6888:6895 LamSF_Tactics <> succ_red constr
R6959:6971 type_derivation <> instance_rule constr
R6983:7001 type_derivation <> quant_preserves_wfs thm
R7012:7015 LamSF_Terms <> lift def
R7026:7047 type_derivation <> lift_rec_preserves_wfs thm
R7058:7062 LamSF_Terms <> subst def
R7065:7068 LamSF_Terms <> lift def
R7079:7103 type_derivation <> subst_rec_preserves_quant thm
R7079:7103 type_derivation <> subst_rec_preserves_quant thm
R7115:7132 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7115:7132 LamSF_Substitution_term <> subst_rec_lift_rec thm
prf 7175:7194 <> instance_quant_lift2
R7221:7228 type_derivation <> instance def
R7251:7252 type_derivation_rwf <> ty var
R7230:7233 LamSF_Terms <> lift def
R7238:7242 type_derivation <> quant def
R7246:7247 type_derivation_rwf <> ty var
R7244:7244 type_derivation_rwf <> n var
R7235:7235 type_derivation_rwf <> n var
R7211:7213 type_derivation <> wfs ind
R7215:7216 type_derivation_rwf <> ty var
R7284:7287 LamSF_Terms <> lift def
R7306:7329 type_derivation <> lift_rec_preserves_quant thm
R7306:7329 type_derivation <> lift_rec_preserves_quant thm
R7342:7342 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7342:7342 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7407:7419 LamSF_Substitution_term <> lift_rec_null thm
R7407:7419 LamSF_Substitution_term <> lift_rec_null thm
R7430:7437 LamSF_Tactics <> zero_red constr
R7457:7464 LamSF_Tactics <> succ_red constr
R7457:7464 LamSF_Tactics <> succ_red constr
R7475:7487 type_derivation <> instance_rule constr
R7475:7487 type_derivation <> instance_rule constr
R7502:7520 type_derivation <> quant_preserves_wfs thm
R7534:7538 LamSF_Terms <> subst def
R7552:7576 type_derivation <> subst_rec_preserves_quant thm
R7552:7576 type_derivation <> subst_rec_preserves_quant thm
R7588:7590 Coq.Init.Logic <> :type_scope:x_'='_x not
R7592:7592 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7588:7590 Coq.Init.Logic <> :type_scope:x_'='_x not
R7592:7592 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7649:7667 LamSF_Substitution_term <> subst_rec_lift_rec3 thm
R7649:7667 LamSF_Substitution_term <> subst_rec_lift_rec3 thm
R7698:7698 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R7698:7698 Coq.Init.Peano <> :nat_scope:x_'+'_x not
prf 7741:7752 <> instance_any
R7788:7795 type_derivation <> instance def
R7814:7815 type_derivation_rwf <> ty var
R7797:7801 type_derivation <> quant def
R7806:7808 LamSF_Terms <> Ref constr
R7810:7810 type_derivation_rwf <> n var
R7803:7803 type_derivation_rwf <> j var
R7778:7780 type_derivation <> wfs ind
R7782:7783 type_derivation_rwf <> ty var
R7772:7772 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7771:7771 type_derivation_rwf <> j var
R7773:7773 type_derivation_rwf <> n var
R7879:7882 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7877:7877 Coq.Init.Logic <> :type_scope:x_'='_x not
R7884:7884 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R7879:7882 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R7877:7877 Coq.Init.Logic <> :type_scope:x_'='_x not
R7884:7884 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8022:8026 LamSF_Terms <> subst def
R8032:8034 LamSF_Terms <> Ref constr
R8022:8026 LamSF_Terms <> subst def
R8032:8034 LamSF_Terms <> Ref constr
R8050:8062 type_derivation <> instance_rule constr
R8108:8112 LamSF_Terms <> subst def
R8118:8120 LamSF_Terms <> Abs constr
R8123:8127 type_derivation <> quant def
R8132:8134 LamSF_Terms <> Ref constr
R8137:8137 Coq.Init.Datatypes <> S constr
R8093:8100 LamSF_Tactics <> succ_red constr
R8108:8112 LamSF_Terms <> subst def
R8118:8120 LamSF_Terms <> Abs constr
R8123:8127 type_derivation <> quant def
R8132:8134 LamSF_Terms <> Ref constr
R8137:8137 Coq.Init.Datatypes <> S constr
R8093:8100 LamSF_Tactics <> succ_red constr
R8162:8174 type_derivation <> instance_rule constr
R8185:8191 type_derivation <> wfs_abs constr
R8202:8220 type_derivation <> quant_preserves_wfs thm
R8231:8235 LamSF_Terms <> subst def
R8253:8277 type_derivation <> subst_rec_preserves_quant thm
R8253:8277 type_derivation <> subst_rec_preserves_quant thm
R8313:8313 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8323:8323 Coq.Init.Datatypes <> S constr
R8323:8323 Coq.Init.Datatypes <> S constr
R8313:8313 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8348:8357 LamSF_Tactics <> multi_step ind
R8370:8372 LamSF_Terms <> Abs constr
R8375:8379 type_derivation <> quant def
R8384:8391 LamSF_Terms <> lift_rec def
R8399:8399 Coq.Init.Datatypes <> S constr
R8359:8367 type_derivation <> instance1 ind
R8418:8425 type_derivation <> instance def
R8427:8431 type_derivation <> quant def
R8440:8443 LamSF_Terms <> lift def
R8446:8446 Coq.Init.Datatypes <> S constr
R8434:8434 Coq.Init.Datatypes <> S constr
R8418:8425 type_derivation <> instance def
R8427:8431 type_derivation <> quant def
R8440:8443 LamSF_Terms <> lift def
R8446:8446 Coq.Init.Datatypes <> S constr
R8434:8434 Coq.Init.Datatypes <> S constr
R8348:8357 LamSF_Tactics <> multi_step ind
R8370:8372 LamSF_Terms <> Abs constr
R8375:8379 type_derivation <> quant def
R8384:8391 LamSF_Terms <> lift_rec def
R8399:8399 Coq.Init.Datatypes <> S constr
R8359:8367 type_derivation <> instance1 ind
R8478:8496 type_derivation_rwf <> instance_quant_lift thm
R8530:8534 LamSF_Terms <> subst def
R8545:8549 type_derivation <> quant def
R8554:8556 LamSF_Terms <> Ref constr
R8537:8539 LamSF_Terms <> Ref constr
R8515:8522 LamSF_Tactics <> succ_red constr
R8530:8534 LamSF_Terms <> subst def
R8545:8549 type_derivation <> quant def
R8554:8556 LamSF_Terms <> Ref constr
R8537:8539 LamSF_Terms <> Ref constr
R8515:8522 LamSF_Tactics <> succ_red constr
R8579:8591 type_derivation <> instance_rule constr
R8602:8620 type_derivation <> quant_preserves_wfs thm
R8631:8635 LamSF_Terms <> subst def
R8653:8677 type_derivation <> subst_rec_preserves_quant thm
R8653:8677 type_derivation <> subst_rec_preserves_quant thm
R8697:8697 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R8697:8697 Coq.Init.Peano <> :nat_scope:x_'+'_x not
prf 8768:8780 <> instance_pull
R8805:8812 type_derivation <> instance def
R8841:8843 Coq.Init.Datatypes <> snd def
R8846:8849 type_derivation_rwf <> pull def
R8851:8852 type_derivation_rwf <> ty var
R8815:8818 LamSF_Terms <> lift def
R8836:8837 type_derivation_rwf <> ty var
R8821:8823 Coq.Init.Datatypes <> fst def
R8826:8829 type_derivation_rwf <> pull def
R8831:8832 type_derivation_rwf <> ty var
R8795:8797 type_derivation <> wfs ind
R8799:8800 type_derivation_rwf <> ty var
R8919:8922 LamSF_Terms <> lift def
R8933:8945 LamSF_Substitution_term <> lift_rec_null thm
R8933:8945 LamSF_Substitution_term <> lift_rec_null thm
R8956:8963 LamSF_Tactics <> zero_red constr
R8983:8986 LamSF_Terms <> lift def
R9004:9029 type_derivation <> preserves_funty_r_instance thm
R9048:9051 LamSF_Terms <> lift def
R9072:9079 LamSF_Tactics <> succ_red constr
R9072:9079 LamSF_Tactics <> succ_red constr
R9090:9102 type_derivation <> instance_rule constr
R9090:9102 type_derivation <> instance_rule constr
R9117:9138 type_derivation <> lift_rec_preserves_wfs thm
R9152:9156 LamSF_Terms <> subst def
R9167:9185 LamSF_Tactics <> subst_rec_lift_rec5 thm
R9167:9185 LamSF_Tactics <> subst_rec_lift_rec5 thm
prf 9221:9240 <> pull_preserves_push1
R9295:9297 Coq.Init.Logic <> :type_scope:x_'='_x not
R9287:9290 type_derivation_rwf <> pull def
R9292:9294 type_derivation_rwf <> ty1 var
R9298:9301 type_derivation_rwf <> pull def
R9303:9305 type_derivation_rwf <> ty2 var
R9270:9274 type_derivation <> push1 ind
R9280:9282 type_derivation_rwf <> ty2 var
R9276:9278 type_derivation_rwf <> ty1 var
R9259:9261 type_derivation <> wfs ind
R9263:9265 type_derivation_rwf <> ty1 var
R9360:9362 type_derivation <> wfs ind
R9360:9362 type_derivation <> wfs ind
R9360:9362 type_derivation <> wfs ind
R9396:9399 LamSF_Terms <> lift def
R9410:9426 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9410:9426 LamSF_Substitution_term <> lift_rec_lift_rec thm
R9462:9463 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9449:9451 Coq.Init.Datatypes <> fst def
R9453:9456 type_derivation_rwf <> pull def
R9473:9473 Coq.Init.Datatypes <> S constr
R9475:9477 Coq.Init.Datatypes <> fst def
R9480:9483 type_derivation_rwf <> pull def
R9473:9473 Coq.Init.Datatypes <> S constr
R9475:9477 Coq.Init.Datatypes <> fst def
R9480:9483 type_derivation_rwf <> pull def
R9462:9463 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9449:9451 Coq.Init.Datatypes <> fst def
R9453:9456 type_derivation_rwf <> pull def
prf 9642:9657 <> resi_implies_rwf
R9721:9734 type_derivation_rwf <> derivation_rwf ind
R9774:9776 Coq.Init.Datatypes <> snd def
R9778:9781 type_derivation_rwf <> pull def
R9783:9784 type_derivation_rwf <> ty var
R9771:9771 type_derivation_rwf <> t var
R9737:9739 Coq.Lists.List <> map def
R9764:9768 type_derivation_rwf <> gamma var
R9742:9745 LamSF_Terms <> lift def
R9748:9750 Coq.Init.Datatypes <> fst def
R9753:9756 type_derivation_rwf <> pull def
R9758:9759 type_derivation_rwf <> ty var
R9710:9712 type_derivation <> wfs ind
R9714:9715 type_derivation_rwf <> ty var
R9680:9694 type_derivation_resi <> derivation_resi ind
R9704:9705 type_derivation_rwf <> ty var
R9702:9702 type_derivation_rwf <> t var
R9696:9700 type_derivation_rwf <> gamma var
R9836:9838 type_derivation <> wfs ind
R9836:9838 type_derivation <> wfs ind
R9836:9838 type_derivation <> wfs ind
R9836:9838 type_derivation <> wfs ind
R9836:9838 type_derivation <> wfs ind
R9836:9838 type_derivation <> wfs ind
R9836:9838 type_derivation <> wfs ind
R9858:9863 type_derivation_rwf <> rwf_op constr
R9874:9887 LamSF_Tactics <> transitive_red thm
R9874:9887 LamSF_Tactics <> transitive_red thm
R9899:9902 type_derivation <> opty def
R9913:9916 LamSF_Terms <> lift def
R9934:9937 type_derivation <> opty def
R9918:9920 Coq.Init.Datatypes <> fst def
R9923:9926 type_derivation_rwf <> pull def
R9954:9957 LamSF_Terms <> lift def
R9913:9916 LamSF_Terms <> lift def
R9934:9937 type_derivation <> opty def
R9918:9920 Coq.Init.Datatypes <> fst def
R9923:9926 type_derivation_rwf <> pull def
R9899:9902 type_derivation <> opty def
R9988:9991 LamSF_Terms <> lift def
R10001:10027 type_derivation <> lift_rec_preserves_instance thm
R10001:10027 type_derivation <> lift_rec_preserves_instance thm
R10050:10062 type_derivation_rwf <> instance_pull thm
R10073:10076 LamSF_Terms <> lift def
R10087:10108 type_derivation <> lift_rec_preserves_wfc thm
R10120:10126 type_derivation_rwf <> pull_wf thm
R10147:10153 type_derivation_rwf <> rwf_var constr
R10164:10177 LamSF_Tactics <> transitive_red thm
R10190:10202 type_derivation_rwf <> instance_pull thm
R10164:10177 LamSF_Tactics <> transitive_red thm
R10190:10202 type_derivation_rwf <> instance_pull thm
R10220:10223 LamSF_Terms <> lift def
R10234:10260 type_derivation <> lift_rec_preserves_instance thm
R10272:10278 type_derivation_rwf <> pull_wf thm
R10289:10292 LamSF_Terms <> lift def
R10303:10324 type_derivation <> lift_rec_preserves_wfc thm
R10345:10352 type_derivation_rwf <> rwf_weak constr
R10363:10366 LamSF_Terms <> lift def
R10377:10398 type_derivation <> lift_rec_preserves_wfs thm
R10419:10425 type_derivation_rwf <> rwf_abs constr
R10491:10497 type_derivation_rwf <> rwf_app constr
R10520:10533 type_derivation_rwf <> derivation_rwf ind
R10584:10588 type_derivation <> funty def
R10619:10621 Coq.Init.Datatypes <> snd def
R10624:10627 type_derivation_rwf <> pull def
R10591:10594 LamSF_Terms <> lift def
R10597:10599 Coq.Init.Datatypes <> fst def
R10602:10605 type_derivation_rwf <> pull def
R10536:10538 Coq.Lists.List <> map def
R10541:10544 LamSF_Terms <> lift def
R10547:10549 Coq.Init.Datatypes <> fst def
R10552:10555 type_derivation_rwf <> pull def
R10520:10533 type_derivation_rwf <> derivation_rwf ind
R10584:10588 type_derivation <> funty def
R10619:10621 Coq.Init.Datatypes <> snd def
R10624:10627 type_derivation_rwf <> pull def
R10591:10594 LamSF_Terms <> lift def
R10597:10599 Coq.Init.Datatypes <> fst def
R10602:10605 type_derivation_rwf <> pull def
R10536:10538 Coq.Lists.List <> map def
R10541:10544 LamSF_Terms <> lift def
R10547:10549 Coq.Init.Datatypes <> fst def
R10552:10555 type_derivation_rwf <> pull def
R10660:10668 type_derivation <> wfs_funty constr
R10680:10698 type_derivation <> derive_implies_wfcs thm
R10721:10724 LamSF_Terms <> lift def
R10735:10762 type_derivation <> lift_rec_ty_preserves_derive thm
R10805:10807 Coq.Lists.List <> map def
R10810:10813 LamSF_Terms <> lift def
R10816:10816 Coq.Init.Datatypes <> S constr
R10819:10821 Coq.Init.Datatypes <> fst def
R10824:10827 type_derivation_rwf <> pull def
R10849:10851 Coq.Lists.List <> map def
R10877:10879 Coq.Lists.List <> map def
R10882:10885 LamSF_Terms <> lift def
R10854:10857 LamSF_Terms <> lift def
R10860:10862 Coq.Init.Datatypes <> fst def
R10865:10868 type_derivation_rwf <> pull def
R10849:10851 Coq.Lists.List <> map def
R10877:10879 Coq.Lists.List <> map def
R10882:10885 LamSF_Terms <> lift def
R10854:10857 LamSF_Terms <> lift def
R10860:10862 Coq.Init.Datatypes <> fst def
R10865:10868 type_derivation_rwf <> pull def
R10805:10807 Coq.Lists.List <> map def
R10810:10813 LamSF_Terms <> lift def
R10816:10816 Coq.Init.Datatypes <> S constr
R10819:10821 Coq.Init.Datatypes <> fst def
R10824:10827 type_derivation_rwf <> pull def
R10975:10978 LamSF_Terms <> lift def
R10989:11005 LamSF_Substitution_term <> lift_rec_lift_rec thm
R10989:11005 LamSF_Substitution_term <> lift_rec_lift_rec thm
R11040:11041 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11028:11030 Coq.Init.Datatypes <> fst def
R11032:11035 type_derivation_rwf <> pull def
R11051:11051 Coq.Init.Datatypes <> S constr
R11053:11055 Coq.Init.Datatypes <> fst def
R11057:11060 type_derivation_rwf <> pull def
R11051:11051 Coq.Init.Datatypes <> S constr
R11053:11055 Coq.Init.Datatypes <> fst def
R11057:11060 type_derivation_rwf <> pull def
R11040:11041 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R11028:11030 Coq.Init.Datatypes <> fst def
R11032:11035 type_derivation_rwf <> pull def
R11106:11125 type_derivation_rwf <> pull_preserves_push1 thm
R11106:11125 type_derivation_rwf <> pull_preserves_push1 thm
R11166:11169 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R11160:11162 type_derivation <> wfs ind
R11170:11172 type_derivation <> wfs ind
R11166:11169 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R11160:11162 type_derivation <> wfs ind
R11170:11172 type_derivation <> wfs ind
R11190:11205 type_derivation <> push_implies_wfs thm
R11233:11236 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R11227:11229 type_derivation <> wfs ind
R11237:11239 type_derivation <> wfs ind
R11233:11236 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R11227:11229 type_derivation <> wfs ind
R11237:11239 type_derivation <> wfs ind
R11257:11272 type_derivation <> push_implies_wfs thm
prf 11302:11319 <> rwf_implies_derive
R11372:11381 type_derivation <> derivation ind
R11391:11392 type_derivation_rwf <> ty var
R11389:11389 type_derivation_rwf <> t var
R11383:11387 type_derivation_rwf <> gamma var
R11343:11356 type_derivation_rwf <> derivation_rwf ind
R11366:11367 type_derivation_rwf <> ty var
R11364:11364 type_derivation_rwf <> t var
R11358:11362 type_derivation_rwf <> gamma var
R11466:11480 type_derivation <> derive_instance thm
R11492:11506 type_derivation <> derive_instance thm
R11517:11526 type_derivation <> derive_var constr
R11537:11556 type_derivation <> instance_implies_wfs thm
R11568:11581 type_derivation <> wf_implies_wfs thm
R11593:11602 type_derivation <> derive_app constr
prf 11621:11631 <> derive_pull
R11733:11742 type_derivation <> derivation ind
R11752:11753 type_derivation_rwf <> ty var
R11750:11750 type_derivation_rwf <> t var
R11744:11748 type_derivation_rwf <> gamma var
R11723:11725 type_derivation <> wfs ind
R11727:11728 type_derivation_rwf <> ty var
R11655:11664 type_derivation <> derivation ind
R11704:11706 Coq.Init.Datatypes <> snd def
R11709:11712 type_derivation_rwf <> pull def
R11714:11715 type_derivation_rwf <> ty var
R11701:11701 type_derivation_rwf <> t var
R11667:11669 Coq.Lists.List <> map def
R11694:11698 type_derivation_rwf <> gamma var
R11672:11675 LamSF_Terms <> lift def
R11678:11680 Coq.Init.Datatypes <> fst def
R11683:11686 type_derivation_rwf <> pull def
R11688:11689 type_derivation_rwf <> ty var
R11913:11922 type_derivation <> derivation ind
R11932:11933 type_derivation_rwf <> ty var
R11930:11930 type_derivation_rwf <> t var
R11924:11928 type_derivation_rwf <> gamma var
R11903:11905 type_derivation <> wfs ind
R11907:11908 type_derivation_rwf <> ty var
R11882:11884 Coq.Init.Logic <> :type_scope:x_'='_x not
R11879:11881 type_derivation_rwf <> ty0 var
R11885:11887 Coq.Init.Datatypes <> snd def
R11890:11893 type_derivation_rwf <> pull def
R11895:11896 type_derivation_rwf <> ty var
R11840:11842 Coq.Init.Logic <> :type_scope:x_'='_x not
R11834:11839 type_derivation_rwf <> gamma0 var
R11843:11845 Coq.Lists.List <> map def
R11870:11874 type_derivation_rwf <> gamma var
R11848:11851 LamSF_Terms <> lift def
R11854:11856 Coq.Init.Datatypes <> fst def
R11859:11862 type_derivation_rwf <> pull def
R11864:11865 type_derivation_rwf <> ty var
R11789:11798 type_derivation <> derivation ind
R11809:11811 type_derivation_rwf <> ty0 var
R11807:11807 type_derivation_rwf <> t var
R11800:11805 type_derivation_rwf <> gamma0 var
R11913:11922 type_derivation <> derivation ind
R11932:11933 type_derivation_rwf <> ty var
R11930:11930 type_derivation_rwf <> t var
R11924:11928 type_derivation_rwf <> gamma var
R11903:11905 type_derivation <> wfs ind
R11907:11908 type_derivation_rwf <> ty var
R11882:11884 Coq.Init.Logic <> :type_scope:x_'='_x not
R11879:11881 type_derivation_rwf <> ty0 var
R11885:11887 Coq.Init.Datatypes <> snd def
R11890:11893 type_derivation_rwf <> pull def
R11895:11896 type_derivation_rwf <> ty var
R11840:11842 Coq.Init.Logic <> :type_scope:x_'='_x not
R11834:11839 type_derivation_rwf <> gamma0 var
R11843:11845 Coq.Lists.List <> map def
R11870:11874 type_derivation_rwf <> gamma var
R11848:11851 LamSF_Terms <> lift def
R11854:11856 Coq.Init.Datatypes <> fst def
R11859:11862 type_derivation_rwf <> pull def
R11864:11865 type_derivation_rwf <> ty var
R11789:11798 type_derivation <> derivation ind
R11809:11811 type_derivation_rwf <> ty0 var
R11807:11807 type_derivation_rwf <> t var
R11800:11805 type_derivation_rwf <> gamma0 var
R12043:12044 type_derivation <> wf ind
R12047:12049 Coq.Init.Datatypes <> snd def
R12052:12055 type_derivation_rwf <> pull def
R12043:12044 type_derivation <> wf ind
R12047:12049 Coq.Init.Datatypes <> snd def
R12052:12055 type_derivation_rwf <> pull def
R12072:12078 type_derivation_rwf <> pull_wf thm
R12130:12133 type_derivation <> opty def
R12136:12141 type_derivation <> op_abs def
R12144:12148 type_derivation <> quant def
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12161:12162 type_derivation <> wf ind
R12236:12246 type_derivation <> derive_push thm
R12236:12246 type_derivation <> derive_push thm
R12260:12269 type_derivation_rwf <> quant_pull thm
R12279:12288 type_derivation <> derive_gen thm
R12279:12288 type_derivation <> derive_gen thm
R12298:12300 Coq.Lists.List <> map def
R12308:12310 Coq.Lists.List <> map def
R12308:12310 Coq.Lists.List <> map def
R12338:12347 type_derivation <> derive_var constr
R12409:12419 type_derivation <> derive_weak constr
R12430:12433 LamSF_Terms <> lift def
R12449:12469 type_derivation <> lift_rec_reflects_wfs thm
R12489:12499 type_derivation <> derive_push thm
R12489:12499 type_derivation <> derive_push thm
R12513:12522 type_derivation_rwf <> quant_pull thm
R12548:12557 type_derivation <> derive_gen thm
R12548:12557 type_derivation <> derive_gen thm
R12568:12577 type_derivation <> derive_abs constr
R12597:12607 type_derivation <> derive_push thm
R12597:12607 type_derivation <> derive_push thm
R12621:12630 type_derivation_rwf <> quant_pull thm
R12641:12650 type_derivation <> derive_gen thm
R12670:12680 type_derivation <> derive_push thm
R12670:12680 type_derivation <> derive_push thm
R12694:12703 type_derivation_rwf <> quant_pull thm
R12714:12723 type_derivation <> derive_gen thm
R12743:12744 type_derivation <> wf ind
R12747:12749 Coq.Init.Datatypes <> snd def
R12752:12755 type_derivation_rwf <> pull def
R12743:12744 type_derivation <> wf ind
R12747:12749 Coq.Init.Datatypes <> snd def
R12752:12755 type_derivation_rwf <> pull def
R12773:12779 type_derivation_rwf <> pull_wf thm
R12808:12809 type_derivation <> wf ind
R12829:12839 type_derivation <> derive_push thm
R12829:12839 type_derivation <> derive_push thm
R12853:12862 type_derivation_rwf <> quant_pull thm
R12873:12882 type_derivation <> derive_gen thm
prf 12900:12932 <> derivation_implies_derivation_rwf
R12990:13003 type_derivation_rwf <> derivation_rwf ind
R13043:13045 Coq.Init.Datatypes <> snd def
R13047:13050 type_derivation_rwf <> pull def
R13052:13053 type_derivation_rwf <> ty var
R13040:13040 type_derivation_rwf <> t var
R13006:13008 Coq.Lists.List <> map def
R13033:13037 type_derivation_rwf <> gamma var
R13011:13014 LamSF_Terms <> lift def
R13017:13019 Coq.Init.Datatypes <> fst def
R13022:13025 type_derivation_rwf <> pull def
R13027:13028 type_derivation_rwf <> ty var
R12979:12981 type_derivation <> wfs ind
R12983:12984 type_derivation_rwf <> ty var
R12954:12963 type_derivation <> derivation ind
R12973:12974 type_derivation_rwf <> ty var
R12971:12971 type_derivation_rwf <> t var
R12965:12969 type_derivation_rwf <> gamma var
R13084:13099 type_derivation_rwf <> resi_implies_rwf thm
R13110:13143 type_derivation_resi <> derivation_implies_derivation_resi thm
prf 13159:13194 <> derivation_implies_derivation_rwf_wf
R13251:13264 type_derivation_rwf <> derivation_rwf ind
R13274:13275 type_derivation_rwf <> ty var
R13272:13272 type_derivation_rwf <> t var
R13266:13270 type_derivation_rwf <> gamma var
R13241:13242 type_derivation <> wf ind
R13244:13245 type_derivation_rwf <> ty var
R13216:13225 type_derivation <> derivation ind
R13235:13236 type_derivation_rwf <> ty var
R13233:13233 type_derivation_rwf <> t var
R13227:13231 type_derivation_rwf <> gamma var
R13306:13319 type_derivation_rwf <> derivation_rwf ind
R13359:13361 Coq.Init.Datatypes <> snd def
R13363:13366 type_derivation_rwf <> pull def
R13322:13324 Coq.Lists.List <> map def
R13327:13330 LamSF_Terms <> lift def
R13333:13335 Coq.Init.Datatypes <> fst def
R13338:13341 type_derivation_rwf <> pull def
R13306:13319 type_derivation_rwf <> derivation_rwf ind
R13359:13361 Coq.Init.Datatypes <> snd def
R13363:13366 type_derivation_rwf <> pull def
R13322:13324 Coq.Lists.List <> map def
R13327:13330 LamSF_Terms <> lift def
R13333:13335 Coq.Init.Datatypes <> fst def
R13338:13341 type_derivation_rwf <> pull def
R13383:13415 type_derivation_rwf <> derivation_implies_derivation_rwf thm
R13426:13439 type_derivation <> wf_implies_wfs thm
R13451:13458 type_derivation_rwf <> pull_wf2 thm
R13451:13458 type_derivation_rwf <> pull_wf2 thm
R13497:13509 type_derivation <> lift0_context thm
R13497:13509 type_derivation <> lift0_context thm
prf 13539:13554 <> rwf_implies_wfcs
R13614:13618 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13605:13607 type_derivation <> wfc ind
R13609:13613 type_derivation_rwf <> gamma var
R13619:13621 type_derivation <> wfs ind
R13623:13624 type_derivation_rwf <> ty var
R13576:13589 type_derivation_rwf <> derivation_rwf ind
R13599:13600 type_derivation_rwf <> ty var
R13597:13597 type_derivation_rwf <> t var
R13591:13595 type_derivation_rwf <> gamma var
R13717:13720 type_derivation <> opty def
R13723:13727 type_derivation <> funty def
R13748:13752 type_derivation <> funty def
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13773:13779 type_derivation <> wfs_abs constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13799:13807 type_derivation <> wfs_funty constr
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13827:13840 type_derivation <> wf_implies_wfs thm
R13862:13869 type_derivation <> wfc_cons constr
R13880:13899 type_derivation <> instance_implies_wfs thm
R13910:13923 type_derivation <> wf_implies_wfs thm
R13942:13942 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13961:13966 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13985:13985 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13954:13956 type_derivation <> wfs ind
R13943:13945 type_derivation <> wfs ind
R13978:13980 type_derivation <> wfs ind
R13967:13969 type_derivation <> wfs ind
R13942:13942 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13961:13966 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13985:13985 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R13954:13956 type_derivation <> wfs ind
R13943:13945 type_derivation <> wfs ind
R13978:13980 type_derivation <> wfs ind
R13967:13969 type_derivation <> wfs ind
R13998:14017 type_derivation <> instance_implies_wfs thm
R14039:14052 type_derivation <> wf_implies_wfs thm
R14128:14136 type_derivation <> wfs_funty constr
prf 14185:14198 <> rwf_implies_wf
R14249:14250 type_derivation <> wf ind
R14252:14253 type_derivation_rwf <> ty var
R14220:14233 type_derivation_rwf <> derivation_rwf ind
R14243:14244 type_derivation_rwf <> ty var
R14241:14241 type_derivation_rwf <> t var
R14235:14239 type_derivation_rwf <> gamma var
R14319:14326 type_derivation <> wf_funty constr
R14336:14338 type_derivation <> wfc ind
R14343:14345 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R14336:14338 type_derivation <> wfc ind
R14343:14345 Coq.Init.Datatypes <> :list_scope:x_'::'_x not
R14365:14380 type_derivation_rwf <> rwf_implies_wfcs thm
prf 14440:14456 <> derive_app_invert
R14537:14543 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R14547:14548 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R14572:14575 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R14549:14558 type_derivation <> derivation ind
R14569:14571 type_derivation_rwf <> ty2 var
R14566:14567 type_derivation_rwf <> t2 var
R14560:14564 type_derivation_rwf <> gamma var
R14576:14585 type_derivation <> derivation ind
R14597:14601 type_derivation <> funty def
R14607:14608 type_derivation_rwf <> ty var
R14603:14605 type_derivation_rwf <> ty2 var
R14593:14594 type_derivation_rwf <> t1 var
R14587:14591 type_derivation_rwf <> gamma var
R14521:14523 Coq.Init.Logic <> :type_scope:x_'='_x not
R14520:14520 type_derivation_rwf <> t var
R14524:14526 LamSF_Terms <> App constr
R14531:14532 type_derivation_rwf <> t2 var
R14528:14529 type_derivation_rwf <> t1 var
R14480:14489 type_derivation <> derivation ind
R14499:14500 type_derivation_rwf <> ty var
R14497:14497 type_derivation_rwf <> t var
R14491:14495 type_derivation_rwf <> gamma var
R14647:14656 type_derivation <> derivation ind
R14705:14708 LamSF_Terms <> lift def
R14711:14713 Coq.Init.Datatypes <> fst def
R14716:14719 type_derivation_rwf <> pull def
R14693:14695 LamSF_Terms <> App constr
R14659:14661 Coq.Lists.List <> map def
R14664:14667 LamSF_Terms <> lift def
R14669:14671 Coq.Init.Datatypes <> fst def
R14674:14677 type_derivation_rwf <> pull def
R14743:14746 LamSF_Terms <> lift def
R14647:14656 type_derivation <> derivation ind