-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsubtypes.glob
1653 lines (1653 loc) · 69.3 KB
/
subtypes.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 0bd3c507147eb1ac0028c4874a62abdb
FTriage.subtypes
R2157:2162 Coq.Strings.String <> <> lib
R2164:2168 Coq.Arith.Arith <> <> lib
R2170:2172 Coq.micromega.Lia <> <> lib
R2174:2177 Coq.Bool.Bool <> <> lib
R2179:2182 Coq.Lists.List <> <> lib
R2184:2186 Coq.Init.Nat <> <> lib
R2204:2208 Triage.terms <> <> lib
R2210:2214 Triage.types <> <> lib
def 2332:2341 <> omega21_ty
R2346:2357 Triage.types <> program_type def
R2359:2365 Triage.terms <> omega21 def
def 2379:2388 <> omega22_ty
R2393:2404 Triage.types <> program_type def
R2406:2412 Triage.terms <> omega22 def
def 2427:2435 <> omega2_ty
R2441:2444 Triage.types <> Fork constr
R2447:2450 Triage.types <> Stem constr
R2452:2461 Triage.subtypes <> omega21_ty def
R2464:2473 Triage.subtypes <> omega22_ty def
def 2489:2495 <> eval_ty
R2500:2504 Triage.types <> quant def
R2509:2513 Triage.types <> Funty constr
R2516:2518 Triage.types <> Var constr
R2524:2526 Triage.types <> Asf constr
R2529:2531 Triage.types <> Var constr
def 2550:2557 <> eager_ty
R2562:2566 Triage.types <> quant def
R2571:2575 Triage.types <> Funty constr
R2578:2582 Triage.types <> Funty constr
R2585:2587 Triage.types <> Var constr
R2593:2595 Triage.types <> Var constr
R2602:2606 Triage.types <> Funty constr
R2609:2611 Triage.types <> Var constr
R2617:2619 Triage.types <> Var constr
def 2639:2646 <> bfff_aug
binder 2648:2650 <> uty:1
R2655:2658 Triage.types <> Fork constr
R2661:2664 Triage.types <> Stem constr
R2667:2670 Triage.types <> Fork constr
R2672:2675 Triage.types <> Leaf constr
R2677:2683 Triage.subtypes <> eval_ty def
R2688:2690 Triage.types <> Asf constr
R2692:2694 Triage.subtypes <> uty:1 var
def 2709:2716 <> bffs_aug
binder 2718:2720 <> uty:2
R2725:2728 Triage.types <> Fork constr
R2731:2734 Triage.types <> Stem constr
R2737:2740 Triage.types <> Fork constr
R2742:2745 Triage.types <> Leaf constr
R2747:2754 Triage.subtypes <> eager_ty def
R2759:2766 Triage.subtypes <> bfff_aug def
R2768:2770 Triage.subtypes <> uty:2 var
ind 2787:2793 <> subtype
constr 2846:2853 <> sub_zero
constr 2884:2892 <> sub_trans
constr 3039:3046 <> sub_stem
constr 3123:3130 <> sub_fork
constr 3289:3295 <> sub_asf
constr 3370:3378 <> sub_funty
constr 3540:3548 <> sub_quant
constr 3665:3678 <> sub_quant_stem
constr 3741:3754 <> sub_quant_fork
constr 3837:3849 <> sub_quant_asf
constr 3910:3917 <> sub_dist
constr 4053:4060 <> sub_inst
constr 4112:4119 <> sub_lift
constr 4218:4229 <> sub_leaf_fun
constr 4282:4293 <> sub_stem_fun
constr 4382:4394 <> sub_fork_leaf
constr 4455:4467 <> sub_fork_stem
constr 4578:4595 <> sub_fork_fork_leaf
constr 4675:4692 <> sub_fork_fork_stem
constr 4806:4823 <> sub_fork_fork_fork
constr 4976:4988 <> sub_recursion
constr 5240:5247 <> sub_tree
constr 5684:5693 <> sub_to_asf
constr 5729:5740 <> sub_from_asf
constr 5807:5814 <> sub_bffs
constr 5910:5917 <> sub_bfff
R2802:2805 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2797:2801 Triage.types <> dtype ind
R2811:2814 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2806:2810 Triage.types <> dtype ind
binder 2864:2865 <> ty:5
R2868:2874 Triage.subtypes <> subtype:3 ind
R2879:2880 Triage.subtypes <> ty:5 var
R2876:2877 Triage.subtypes <> ty:5 var
binder 2903:2905 <> ty1:6
binder 2907:2909 <> ty2:7
binder 2911:2913 <> ty3:8
R2931:2934 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2916:2922 Triage.subtypes <> subtype:3 ind
R2928:2930 Triage.subtypes <> ty2:7 var
R2924:2926 Triage.subtypes <> ty1:6 var
R2950:2953 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R2935:2941 Triage.subtypes <> subtype:3 ind
R2947:2949 Triage.subtypes <> ty3:8 var
R2943:2945 Triage.subtypes <> ty2:7 var
R2954:2960 Triage.subtypes <> subtype:3 ind
R2966:2968 Triage.subtypes <> ty3:8 var
R2962:2964 Triage.subtypes <> ty1:6 var
binder 3057:3060 <> uty1:9
binder 3062:3065 <> uty2:10
R3085:3088 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3068:3074 Triage.subtypes <> subtype:3 ind
R3081:3084 Triage.subtypes <> uty2:10 var
R3076:3079 Triage.subtypes <> uty1:9 var
R3089:3095 Triage.subtypes <> subtype:3 ind
R3110:3113 Triage.types <> Stem constr
R3115:3118 Triage.subtypes <> uty2:10 var
R3098:3101 Triage.types <> Stem constr
R3103:3106 Triage.subtypes <> uty1:9 var
binder 3141:3144 <> uty1:11
binder 3146:3149 <> uty2:12
binder 3151:3154 <> vty1:13
binder 3156:3159 <> vty2:14
R3179:3182 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3162:3168 Triage.subtypes <> subtype:3 ind
R3175:3178 Triage.subtypes <> uty2:12 var
R3170:3173 Triage.subtypes <> uty1:11 var
R3200:3244 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3183:3189 Triage.subtypes <> subtype:3 ind
R3196:3199 Triage.subtypes <> vty2:14 var
R3191:3194 Triage.subtypes <> vty1:13 var
R3245:3251 Triage.subtypes <> subtype:3 ind
R3271:3274 Triage.types <> Fork constr
R3276:3279 Triage.subtypes <> uty2:12 var
R3281:3284 Triage.subtypes <> vty2:14 var
R3254:3257 Triage.types <> Fork constr
R3259:3262 Triage.subtypes <> uty1:11 var
R3264:3267 Triage.subtypes <> vty1:13 var
binder 3306:3309 <> uty1:15
binder 3311:3314 <> uty2:16
R3334:3337 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3317:3323 Triage.subtypes <> subtype:3 ind
R3330:3333 Triage.subtypes <> uty2:16 var
R3325:3328 Triage.subtypes <> uty1:15 var
R3338:3344 Triage.subtypes <> subtype:3 ind
R3358:3360 Triage.types <> Asf constr
R3362:3365 Triage.subtypes <> uty2:16 var
R3347:3349 Triage.types <> Asf constr
R3351:3354 Triage.subtypes <> uty1:15 var
binder 3389:3392 <> uty1:17
binder 3394:3397 <> uty2:18
binder 3399:3402 <> vty1:19
binder 3404:3407 <> vty2:20
R3427:3430 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3410:3416 Triage.subtypes <> subtype:3 ind
R3423:3426 Triage.subtypes <> uty1:17 var
R3418:3421 Triage.subtypes <> uty2:18 var
R3448:3493 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3431:3437 Triage.subtypes <> subtype:3 ind
R3444:3447 Triage.subtypes <> vty2:20 var
R3439:3442 Triage.subtypes <> vty1:19 var
R3494:3500 Triage.subtypes <> subtype:3 ind
R3521:3525 Triage.types <> Funty constr
R3527:3530 Triage.subtypes <> uty2:18 var
R3532:3535 Triage.subtypes <> vty2:20 var
R3503:3507 Triage.types <> Funty constr
R3509:3512 Triage.subtypes <> uty1:17 var
R3514:3517 Triage.subtypes <> vty1:19 var
binder 3559:3562 <> vty1:21
binder 3564:3567 <> vty2:22
R3588:3591 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R3571:3577 Triage.subtypes <> subtype:3 ind
R3584:3587 Triage.subtypes <> vty2:22 var
R3579:3582 Triage.subtypes <> vty1:21 var
R3592:3598 Triage.subtypes <> subtype:3 ind
R3614:3618 Triage.types <> Quant constr
R3620:3623 Triage.subtypes <> vty2:22 var
R3601:3605 Triage.types <> Quant constr
R3607:3610 Triage.subtypes <> vty1:21 var
binder 3688:3690 <> uty:23
R3693:3699 Triage.subtypes <> subtype:3 ind
R3721:3724 Triage.types <> Stem constr
R3727:3731 Triage.types <> Quant constr
R3733:3735 Triage.subtypes <> uty:23 var
R3702:3706 Triage.types <> Quant constr
R3709:3712 Triage.types <> Stem constr
R3714:3716 Triage.subtypes <> uty:23 var
binder 3764:3766 <> uty:24
binder 3768:3770 <> vty:25
R3773:3779 Triage.subtypes <> subtype:3 ind
R3805:3808 Triage.types <> Fork constr
R3811:3815 Triage.types <> Quant constr
R3817:3819 Triage.subtypes <> uty:24 var
R3823:3827 Triage.types <> Quant constr
R3829:3831 Triage.subtypes <> vty:25 var
R3782:3786 Triage.types <> Quant constr
R3789:3792 Triage.types <> Fork constr
R3794:3796 Triage.subtypes <> uty:24 var
R3798:3800 Triage.subtypes <> vty:25 var
binder 3859:3861 <> uty:26
R3864:3870 Triage.subtypes <> subtype:3 ind
R3891:3893 Triage.types <> Asf constr
R3896:3900 Triage.types <> Quant constr
R3902:3904 Triage.subtypes <> uty:26 var
R3873:3877 Triage.types <> Quant constr
R3880:3882 Triage.types <> Asf constr
R3884:3886 Triage.subtypes <> uty:26 var
binder 3927:3929 <> uty:27
binder 3931:3933 <> vty:28
R3936:3942 Triage.subtypes <> subtype:3 ind
R3969:3973 Triage.types <> Funty constr
R3976:3980 Triage.types <> Quant constr
R3982:3984 Triage.subtypes <> uty:27 var
R3988:3992 Triage.types <> Quant constr
R3994:3996 Triage.subtypes <> vty:28 var
R3945:3949 Triage.types <> Quant constr
R3952:3956 Triage.types <> Funty constr
R3958:3960 Triage.subtypes <> uty:27 var
R3962:3964 Triage.subtypes <> vty:28 var
binder 4071:4072 <> ty:29
binder 4074:4074 <> u:30
R4078:4084 Triage.subtypes <> subtype:3 ind
R4098:4102 Triage.types <> subst def
R4104:4105 Triage.subtypes <> ty:29 var
R4107:4107 Triage.subtypes <> u:30 var
R4087:4091 Triage.types <> Quant constr
R4093:4094 Triage.subtypes <> ty:29 var
binder 4129:4130 <> ty:31
R4133:4139 Triage.subtypes <> subtype:3 ind
R4145:4149 Triage.types <> Quant constr
R4152:4155 Triage.types <> lift def
R4159:4160 Triage.subtypes <> ty:31 var
R4141:4142 Triage.subtypes <> ty:31 var
binder 4238:4240 <> uty:32
R4244:4250 Triage.subtypes <> subtype:3 ind
R4258:4262 Triage.types <> Funty constr
R4264:4266 Triage.subtypes <> uty:32 var
R4269:4272 Triage.types <> Stem constr
R4274:4276 Triage.subtypes <> uty:32 var
R4252:4255 Triage.types <> Leaf constr
binder 4303:4305 <> uty:33
binder 4307:4309 <> vty:34
R4312:4318 Triage.subtypes <> subtype:3 ind
R4332:4336 Triage.types <> Funty constr
R4338:4340 Triage.subtypes <> vty:34 var
R4343:4346 Triage.types <> Fork constr
R4348:4350 Triage.subtypes <> uty:33 var
R4352:4354 Triage.subtypes <> vty:34 var
R4321:4324 Triage.types <> Stem constr
R4326:4328 Triage.subtypes <> uty:33 var
binder 4404:4406 <> uty:35
binder 4408:4410 <> vty:36
R4413:4419 Triage.subtypes <> subtype:3 ind
R4438:4442 Triage.types <> Funty constr
R4444:4446 Triage.subtypes <> vty:36 var
R4448:4450 Triage.subtypes <> uty:35 var
R4422:4425 Triage.types <> Fork constr
R4427:4430 Triage.types <> Leaf constr
R4432:4434 Triage.subtypes <> uty:35 var
binder 4477:4479 <> uty:37
binder 4481:4483 <> vty:38
binder 4485:4487 <> wty:39
R4494:4500 Triage.subtypes <> subtype:3 ind
R4561:4565 Triage.types <> Funty constr
R4567:4569 Triage.subtypes <> uty:37 var
R4571:4573 Triage.subtypes <> wty:39 var
R4503:4506 Triage.types <> Fork constr
R4509:4512 Triage.types <> Stem constr
R4515:4519 Triage.types <> Funty constr
R4521:4523 Triage.subtypes <> uty:37 var
R4526:4530 Triage.types <> Funty constr
R4532:4534 Triage.subtypes <> vty:38 var
R4536:4538 Triage.subtypes <> wty:39 var
R4544:4548 Triage.types <> Funty constr
R4550:4552 Triage.subtypes <> uty:37 var
R4554:4556 Triage.subtypes <> vty:38 var
binder 4605:4607 <> uty:40
binder 4609:4611 <> vty:41
binder 4613:4615 <> wty:42
R4622:4628 Triage.subtypes <> subtype:3 ind
R4657:4661 Triage.types <> Funty constr
R4663:4666 Triage.types <> Leaf constr
R4668:4670 Triage.subtypes <> uty:40 var
R4631:4634 Triage.types <> Fork constr
R4637:4640 Triage.types <> Fork constr
R4642:4644 Triage.subtypes <> uty:40 var
R4646:4648 Triage.subtypes <> vty:41 var
R4651:4653 Triage.subtypes <> wty:42 var
binder 4706:4708 <> uty:43
binder 4710:4713 <> vty1:44
binder 4715:4718 <> vty2:45
binder 4720:4722 <> wty:46
R4731:4737 Triage.subtypes <> subtype:3 ind
R4780:4784 Triage.types <> Funty constr
R4787:4790 Triage.types <> Stem constr
R4792:4795 Triage.subtypes <> vty1:44 var
R4798:4801 Triage.subtypes <> vty2:45 var
R4740:4743 Triage.types <> Fork constr
R4746:4749 Triage.types <> Fork constr
R4751:4753 Triage.subtypes <> uty:43 var
R4756:4760 Triage.types <> Funty constr
R4762:4765 Triage.subtypes <> vty1:44 var
R4767:4770 Triage.subtypes <> vty2:45 var
R4774:4776 Triage.subtypes <> wty:46 var
binder 4837:4839 <> uty:47
binder 4841:4843 <> vty:48
binder 4845:4848 <> wty1:49
binder 4850:4853 <> wty2:50
binder 4855:4858 <> wty3:51
R4867:4873 Triage.subtypes <> subtype:3 ind
R4929:4933 Triage.types <> Funty constr
R4936:4939 Triage.types <> Fork constr
R4941:4944 Triage.subtypes <> wty1:49 var
R4946:4949 Triage.subtypes <> wty2:50 var
R4952:4955 Triage.subtypes <> wty3:51 var
R4876:4879 Triage.types <> Fork constr
R4882:4885 Triage.types <> Fork constr
R4887:4889 Triage.subtypes <> uty:47 var
R4891:4893 Triage.subtypes <> vty:48 var
R4897:4901 Triage.types <> Funty constr
R4903:4906 Triage.subtypes <> wty1:49 var
R4909:4913 Triage.types <> Funty constr
R4915:4918 Triage.subtypes <> wty2:50 var
R4920:4923 Triage.subtypes <> wty3:51 var
binder 5002:5002 <> k:52
binder 5004:5006 <> uty:53
binder 5008:5010 <> vty:54
R5019:5025 Triage.subtypes <> subtype:3 ind
R5052:5056 Triage.types <> Funty constr
R5075:5083 Triage.subtypes <> omega2_ty def
R5103:5107 Triage.types <> Funty constr
R5130:5134 Triage.types <> Funty constr
R5137:5141 Triage.types <> quant def
R5143:5143 Triage.subtypes <> k:52 var
R5146:5150 Triage.types <> Funty constr
R5152:5154 Triage.subtypes <> uty:53 var
R5156:5158 Triage.subtypes <> vty:54 var
R5163:5167 Triage.types <> quant def
R5169:5169 Triage.subtypes <> k:52 var
R5172:5176 Triage.types <> Funty constr
R5178:5180 Triage.subtypes <> uty:53 var
R5182:5184 Triage.subtypes <> vty:54 var
R5210:5214 Triage.types <> quant def
R5216:5216 Triage.subtypes <> k:52 var
R5219:5223 Triage.types <> Funty constr
R5225:5227 Triage.subtypes <> uty:53 var
R5229:5231 Triage.subtypes <> vty:54 var
R5027:5035 Triage.subtypes <> omega2_ty def
binder 5257:5258 <> ty:55
binder 5260:5262 <> uty:56
R5281:5289 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R5269:5277 Triage.types <> covariant def
R5279:5280 Triage.subtypes <> ty:55 var
R5290:5296 Triage.subtypes <> subtype:3 ind
R5656:5660 Triage.types <> Funty constr
R5662:5664 Triage.subtypes <> uty:56 var
R5667:5671 Triage.types <> subst def
R5673:5674 Triage.subtypes <> ty:55 var
R5676:5678 Triage.subtypes <> uty:56 var
R5299:5302 Triage.types <> Fork constr
R5320:5323 Triage.types <> Fork constr
R5344:5348 Triage.types <> subst def
R5350:5351 Triage.subtypes <> ty:55 var
R5353:5356 Triage.types <> Leaf constr
R5378:5382 Triage.types <> quant def
R5387:5391 Triage.types <> Funty constr
R5394:5396 Triage.types <> Var constr
R5402:5406 Triage.types <> subst def
R5409:5416 Triage.types <> lift_rec def
R5418:5419 Triage.subtypes <> ty:55 var
R5427:5430 Triage.types <> Stem constr
R5433:5435 Triage.types <> Var constr
R5461:5465 Triage.types <> quant def
R5506:5510 Triage.types <> Funty constr
R5534:5536 Triage.types <> Var constr
R5563:5567 Triage.types <> Funty constr
R5570:5572 Triage.types <> Var constr
R5578:5582 Triage.types <> subst def
R5585:5592 Triage.types <> lift_rec def
R5594:5595 Triage.subtypes <> ty:55 var
R5603:5606 Triage.types <> Fork constr
R5609:5611 Triage.types <> Var constr
R5617:5619 Triage.types <> Var constr
binder 5703:5704 <> ty:57
R5707:5713 Triage.subtypes <> subtype:3 ind
R5719:5721 Triage.types <> Asf constr
R5723:5724 Triage.subtypes <> ty:57 var
R5715:5716 Triage.subtypes <> ty:57 var
binder 5750:5752 <> uty:58
binder 5754:5756 <> vty:59
R5759:5765 Triage.subtypes <> subtype:3 ind
R5790:5794 Triage.types <> Funty constr
R5796:5798 Triage.subtypes <> uty:58 var
R5800:5802 Triage.subtypes <> vty:59 var
R5768:5770 Triage.types <> Asf constr
R5773:5777 Triage.types <> Funty constr
R5779:5781 Triage.subtypes <> uty:58 var
R5783:5785 Triage.subtypes <> vty:59 var
binder 5824:5826 <> uty:60
binder 5828:5830 <> vty:61
R5833:5839 Triage.subtypes <> subtype:3 ind
R5881:5883 Triage.types <> Asf constr
R5886:5889 Triage.types <> Fork constr
R5892:5895 Triage.types <> Stem constr
R5897:5899 Triage.subtypes <> uty:60 var
R5902:5904 Triage.subtypes <> vty:61 var
R5842:5845 Triage.types <> Fork constr
R5848:5851 Triage.types <> Stem constr
R5854:5861 Triage.subtypes <> bffs_aug def
R5863:5865 Triage.subtypes <> uty:60 var
R5870:5872 Triage.types <> Asf constr
R5874:5876 Triage.subtypes <> vty:61 var
binder 5928:5930 <> uty:62
binder 5932:5934 <> vty:63
binder 5936:5938 <> wty:64
R5941:5947 Triage.subtypes <> subtype:3 ind
R6034:6036 Triage.types <> Asf constr
R6039:6042 Triage.types <> Fork constr
R6045:6048 Triage.types <> Fork constr
R6050:6052 Triage.subtypes <> uty:62 var
R6054:6056 Triage.subtypes <> vty:63 var
R6059:6061 Triage.subtypes <> wty:64 var
R5950:5953 Triage.types <> Fork constr
R5956:5959 Triage.types <> Fork constr
R5961:5963 Triage.subtypes <> uty:62 var
R5966:5968 Triage.types <> Asf constr
R5970:5972 Triage.subtypes <> vty:63 var
R5977:5984 Triage.subtypes <> bfff_aug def
R5986:5988 Triage.subtypes <> wty:64 var
R6094:6100 Triage.subtypes <> subtype ind
R6143:6147 Triage.types <> subst def
R6150:6153 Triage.types <> lift def
R6209:6226 Triage.types <> subst_rec_lift_rec thm
R6304:6307 Triage.types <> lift def
R6320:6332 Triage.types <> lift_rec_null thm
R6346:6353 Triage.subtypes <> sub_zero constr
R6436:6444 Triage.subtypes <> sub_funty constr
R6458:6465 Triage.subtypes <> sub_zero constr
R6389:6397 Triage.subtypes <> sub_funty constr
R6409:6416 Triage.subtypes <> sub_zero constr
R6499:6507 Triage.subtypes <> sub_trans constr
R6519:6526 Triage.subtypes <> sub_inst constr
prf 6549:6561 <> subtype_quant
binder 6573:6573 <> n:65
binder 6575:6577 <> uty:66
binder 6579:6581 <> vty:67
R6600:6603 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6585:6591 Triage.subtypes <> subtype ind
R6593:6595 Triage.subtypes <> uty:66 var
R6597:6599 Triage.subtypes <> vty:67 var
R6604:6610 Triage.subtypes <> subtype ind
R6613:6617 Triage.types <> quant def
R6619:6619 Triage.subtypes <> n:65 var
R6621:6623 Triage.subtypes <> uty:66 var
R6627:6631 Triage.types <> quant def
R6633:6633 Triage.subtypes <> n:65 var
R6635:6637 Triage.subtypes <> vty:67 var
prf 6721:6734 <> subtype_quanta
binder 6744:6745 <> bs:68
binder 6747:6749 <> ty1:69
binder 6751:6753 <> ty2:70
R6771:6774 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R6756:6762 Triage.subtypes <> subtype ind
R6764:6766 Triage.subtypes <> ty1:69 var
R6768:6770 Triage.subtypes <> ty2:70 var
R6775:6781 Triage.subtypes <> subtype ind
R6784:6789 Triage.types <> quanta def
R6791:6792 Triage.subtypes <> bs:68 var
R6794:6796 Triage.subtypes <> ty1:69 var
R6800:6805 Triage.types <> quanta def
R6807:6808 Triage.subtypes <> bs:68 var
R6810:6812 Triage.subtypes <> ty2:70 var
prf 6906:6917 <> subtype_dist
binder 6927:6927 <> n:71
binder 6929:6931 <> uty:72
binder 6933:6935 <> vty:73
R6939:6945 Triage.subtypes <> subtype ind
R6948:6952 Triage.types <> quant def
R6954:6954 Triage.subtypes <> n:71 var
R6957:6961 Triage.types <> Funty constr
R6963:6965 Triage.subtypes <> uty:72 var
R6967:6969 Triage.subtypes <> vty:73 var
R6974:6978 Triage.types <> Funty constr
R6981:6985 Triage.types <> quant def
R6987:6987 Triage.subtypes <> n:71 var
R6989:6991 Triage.subtypes <> uty:72 var
R6995:6999 Triage.types <> quant def
R7001:7001 Triage.subtypes <> n:71 var
R7003:7005 Triage.subtypes <> vty:73 var
R7063:7070 Triage.subtypes <> sub_zero constr
R7084:7092 Triage.subtypes <> sub_trans constr
R7104:7116 Triage.subtypes <> subtype_quant thm
R7126:7133 Triage.subtypes <> sub_dist constr
R7063:7070 Triage.subtypes <> sub_zero constr
R7063:7070 Triage.subtypes <> sub_zero constr
R7084:7092 Triage.subtypes <> sub_trans constr
R7104:7116 Triage.subtypes <> subtype_quant thm
R7126:7133 Triage.subtypes <> sub_dist constr
prf 7161:7183 <> subtype_quant_to_quanta
binder 7193:7194 <> bs:74
binder 7196:7197 <> ty:75
R7201:7207 Triage.subtypes <> subtype ind
R7210:7214 Triage.types <> quant def
R7217:7227 Triage.types <> quant_count def
R7229:7230 Triage.subtypes <> bs:74 var
R7233:7234 Triage.subtypes <> ty:75 var
R7238:7243 Triage.types <> quanta def
R7245:7246 Triage.subtypes <> bs:74 var
R7248:7249 Triage.subtypes <> ty:75 var
R7348:7356 Triage.subtypes <> sub_trans constr
R7368:7380 Triage.subtypes <> subtype_quant thm
R7390:7399 Triage.subtypes <> sub_to_asf constr
R7348:7356 Triage.subtypes <> sub_trans constr
R7368:7380 Triage.subtypes <> subtype_quant thm
R7390:7399 Triage.subtypes <> sub_to_asf constr
prf 7425:7450 <> lift_rec_preserves_subtype
binder 7462:7464 <> ty1:76
binder 7466:7468 <> ty2:77
R7486:7489 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R7471:7477 Triage.subtypes <> subtype ind
R7479:7481 Triage.subtypes <> ty1:76 var
R7483:7485 Triage.subtypes <> ty2:77 var
binder 7497:7497 <> n:78
binder 7499:7499 <> k:79
R7502:7508 Triage.subtypes <> subtype ind
R7511:7518 Triage.types <> lift_rec def
R7520:7522 Triage.subtypes <> ty1:76 var
R7524:7524 Triage.subtypes <> n:78 var
R7526:7526 Triage.subtypes <> k:79 var
R7530:7537 Triage.types <> lift_rec def
R7539:7541 Triage.subtypes <> ty2:77 var
R7543:7543 Triage.subtypes <> n:78 var
R7545:7545 Triage.subtypes <> k:79 var
R7643:7646 Triage.types <> lift def
R7659:7671 Triage.types <> lift_lift_rec thm
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7604:7611 Triage.types <> lift_rec def
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7659:7671 Triage.types <> lift_lift_rec thm
R7742:7742 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R7767:7784 Triage.types <> lift_rec_subst_rec thm
R7742:7742 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R7767:7784 Triage.types <> lift_rec_subst_rec thm
R7767:7784 Triage.types <> lift_rec_subst_rec thm
R7810:7817 Triage.types <> lift_rec def
R7819:7827 Triage.subtypes <> omega2_ty def
R7840:7848 Triage.subtypes <> omega2_ty def
R7882:7905 Triage.types <> lift_rec_preserves_quant thm
R7915:7927 Triage.subtypes <> sub_recursion constr
R7810:7817 Triage.types <> lift_rec def
R7819:7827 Triage.subtypes <> omega2_ty def
R7840:7848 Triage.subtypes <> omega2_ty def
R7882:7905 Triage.types <> lift_rec_preserves_quant thm
R7882:7905 Triage.types <> lift_rec_preserves_quant thm
R7882:7905 Triage.types <> lift_rec_preserves_quant thm
R7915:7927 Triage.subtypes <> sub_recursion constr
R7956:7964 Triage.subtypes <> sub_trans constr
R7984:7992 Triage.subtypes <> sub_trans constr
R8006:8013 Triage.subtypes <> sub_tree constr
R8048:8052 Triage.types <> subst def
R8072:8072 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8097:8114 Triage.types <> lift_rec_subst_rec thm
R8124:8131 Triage.subtypes <> sub_zero constr
R8160:8168 Triage.types <> covariant def
R8199:8206 Triage.types <> relocate def
R8211:8211 Coq.Init.Datatypes <> S constr
R8244:8269 Triage.types <> lift_rec_preserves_variant thm
R8292:8299 Triage.subtypes <> sub_fork constr
R8311:8318 Triage.subtypes <> sub_fork constr
R8341:8345 Triage.types <> subst def
R8365:8365 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8390:8407 Triage.types <> lift_rec_subst_rec thm
R8417:8424 Triage.subtypes <> sub_zero constr
R8455:8455 Coq.Init.Datatypes <> S constr
R8467:8468 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8469:8469 Coq.Init.Datatypes <> S constr
R8498:8515 Triage.types <> lift_rec_subst_rec thm
R8545:8557 Triage.types <> lift_lift_rec thm
R8593:8597 Triage.types <> subst def
R8625:8625 Coq.Init.Datatypes <> S constr
R8628:8628 Coq.Init.Datatypes <> S constr
R8641:8642 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8643:8643 Coq.Init.Datatypes <> S constr
R8646:8646 Coq.Init.Datatypes <> S constr
R8680:8697 Triage.types <> lift_rec_subst_rec thm
R8740:8740 Coq.Init.Datatypes <> S constr
R8743:8743 Coq.Init.Datatypes <> S constr
R8746:8746 Coq.Init.Datatypes <> S constr
R8760:8762 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8763:8763 Coq.Init.Datatypes <> S constr
R8785:8797 Triage.types <> lift_lift_rec thm
R7956:7964 Triage.subtypes <> sub_trans constr
R7984:7992 Triage.subtypes <> sub_trans constr
R8006:8013 Triage.subtypes <> sub_tree constr
R8072:8072 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8097:8114 Triage.types <> lift_rec_subst_rec thm
R8097:8114 Triage.types <> lift_rec_subst_rec thm
R8124:8131 Triage.subtypes <> sub_zero constr
R8199:8206 Triage.types <> relocate def
R8211:8211 Coq.Init.Datatypes <> S constr
R8244:8269 Triage.types <> lift_rec_preserves_variant thm
R8244:8269 Triage.types <> lift_rec_preserves_variant thm
R8292:8299 Triage.subtypes <> sub_fork constr
R8311:8318 Triage.subtypes <> sub_fork constr
R8365:8365 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8390:8407 Triage.types <> lift_rec_subst_rec thm
R8390:8407 Triage.types <> lift_rec_subst_rec thm
R8417:8424 Triage.subtypes <> sub_zero constr
R8455:8455 Coq.Init.Datatypes <> S constr
R8467:8468 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8469:8469 Coq.Init.Datatypes <> S constr
R8498:8515 Triage.types <> lift_rec_subst_rec thm
R8498:8515 Triage.types <> lift_rec_subst_rec thm
R8545:8557 Triage.types <> lift_lift_rec thm
R8545:8557 Triage.types <> lift_lift_rec thm
R8545:8557 Triage.types <> lift_lift_rec thm
R8625:8625 Coq.Init.Datatypes <> S constr
R8628:8628 Coq.Init.Datatypes <> S constr
R8641:8642 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8643:8643 Coq.Init.Datatypes <> S constr
R8646:8646 Coq.Init.Datatypes <> S constr
R8680:8697 Triage.types <> lift_rec_subst_rec thm
R8680:8697 Triage.types <> lift_rec_subst_rec thm
R8740:8740 Coq.Init.Datatypes <> S constr
R8743:8743 Coq.Init.Datatypes <> S constr
R8746:8746 Coq.Init.Datatypes <> S constr
R8760:8762 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R8763:8763 Coq.Init.Datatypes <> S constr
R8785:8797 Triage.types <> lift_lift_rec thm
R8785:8797 Triage.types <> lift_lift_rec thm
R8785:8797 Triage.types <> lift_lift_rec thm
R8830:8837 Triage.subtypes <> bffs_aug def
R8840:8847 Triage.subtypes <> bfff_aug def
R8874:8881 Triage.subtypes <> sub_bffs constr
R8874:8881 Triage.subtypes <> sub_bffs constr
R8895:8902 Triage.subtypes <> bffs_aug def
R8905:8912 Triage.subtypes <> bfff_aug def
R8939:8946 Triage.subtypes <> sub_bfff constr
R8939:8946 Triage.subtypes <> sub_bfff constr
prf 8962:8988 <> subst_rec_preserves_subtype
binder 9000:9002 <> uty:80
binder 9004:9006 <> vty:81
R9024:9027 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R9009:9015 Triage.subtypes <> subtype ind
R9017:9019 Triage.subtypes <> uty:80 var
R9021:9023 Triage.subtypes <> vty:81 var
binder 9035:9036 <> ty:82
binder 9038:9038 <> k:83
R9041:9047 Triage.subtypes <> subtype ind
R9050:9058 Triage.types <> subst_rec def
R9060:9062 Triage.subtypes <> uty:80 var
R9064:9065 Triage.subtypes <> ty:82 var
R9067:9067 Triage.subtypes <> k:83 var
R9071:9079 Triage.types <> subst_rec def
R9081:9083 Triage.subtypes <> vty:81 var
R9085:9086 Triage.subtypes <> ty:82 var
R9088:9088 Triage.subtypes <> k:83 var
R9147:9150 Triage.types <> lift def
R9207:9210 Triage.types <> lift def
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9164:9172 Triage.types <> subst_rec def
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9223:9241 Triage.types <> subst_rec_lift_rec1 thm
R9300:9308 Triage.subtypes <> sub_trans constr
R9323:9341 Triage.types <> subst_rec_subst_rec thm
R9361:9368 Triage.subtypes <> sub_zero constr
R9300:9308 Triage.subtypes <> sub_trans constr
R9323:9341 Triage.types <> subst_rec_subst_rec thm
R9323:9341 Triage.types <> subst_rec_subst_rec thm
R9323:9341 Triage.types <> subst_rec_subst_rec thm
R9361:9368 Triage.subtypes <> sub_zero constr
R9361:9368 Triage.subtypes <> sub_zero constr
R9385:9393 Triage.types <> subst_rec def
R9395:9403 Triage.subtypes <> omega2_ty def
R9417:9425 Triage.subtypes <> omega2_ty def
R9459:9483 Triage.types <> subst_rec_preserves_quant thm
R9493:9505 Triage.subtypes <> sub_recursion constr
R9385:9393 Triage.types <> subst_rec def
R9395:9403 Triage.subtypes <> omega2_ty def
R9417:9425 Triage.subtypes <> omega2_ty def
R9459:9483 Triage.types <> subst_rec_preserves_quant thm
R9459:9483 Triage.types <> subst_rec_preserves_quant thm
R9459:9483 Triage.types <> subst_rec_preserves_quant thm
R9493:9505 Triage.subtypes <> sub_recursion constr
R9519:9523 Triage.types <> subst def
R9534:9552 Triage.types <> subst_rec_subst_rec thm
R9580:9580 Coq.Init.Nat <> ::nat_scope:x_'-'_x not
R9612:9620 Triage.subtypes <> sub_trans constr
R9632:9640 Triage.subtypes <> sub_trans constr
R9654:9661 Triage.subtypes <> sub_tree constr
R9685:9692 Triage.subtypes <> sub_fork constr
R9714:9721 Triage.subtypes <> sub_fork constr
R9752:9759 Triage.subtypes <> sub_zero constr
R9799:9817 Triage.types <> subst_rec_subst_rec thm
R9865:9883 Triage.types <> subst_rec_lift_rec1 thm
R9909:9916 Triage.subtypes <> sub_zero constr
R9956:9974 Triage.types <> subst_rec_subst_rec thm
R10019:10019 Coq.Init.Datatypes <> S constr
R10022:10022 Coq.Init.Datatypes <> S constr
R10025:10025 Coq.Init.Datatypes <> S constr
R10039:10041 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10042:10042 Coq.Init.Datatypes <> S constr
R10071:10089 Triage.types <> subst_rec_lift_rec1 thm
R10115:10122 Triage.subtypes <> sub_zero constr
R10142:10150 Triage.types <> covariant def
R10175:10175 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10195:10216 Triage.types <> variant_subst_rec_miss thm
R10256:10260 Triage.types <> subst def
R10272:10290 Triage.types <> subst_rec_subst_rec thm
R10327:10327 Coq.Init.Nat <> ::nat_scope:x_'-'_x not
R10353:10360 Triage.subtypes <> sub_zero constr
R9534:9552 Triage.types <> subst_rec_subst_rec thm
R9534:9552 Triage.types <> subst_rec_subst_rec thm
R9534:9552 Triage.types <> subst_rec_subst_rec thm
R9580:9580 Coq.Init.Nat <> ::nat_scope:x_'-'_x not
R9612:9620 Triage.subtypes <> sub_trans constr
R9632:9640 Triage.subtypes <> sub_trans constr
R9654:9661 Triage.subtypes <> sub_tree constr
R9685:9692 Triage.subtypes <> sub_fork constr
R9714:9721 Triage.subtypes <> sub_fork constr
R9752:9759 Triage.subtypes <> sub_zero constr
R9799:9817 Triage.types <> subst_rec_subst_rec thm
R9799:9817 Triage.types <> subst_rec_subst_rec thm
R9799:9817 Triage.types <> subst_rec_subst_rec thm
R9865:9883 Triage.types <> subst_rec_lift_rec1 thm
R9865:9883 Triage.types <> subst_rec_lift_rec1 thm
R9865:9883 Triage.types <> subst_rec_lift_rec1 thm
R9909:9916 Triage.subtypes <> sub_zero constr
R9956:9974 Triage.types <> subst_rec_subst_rec thm
R9956:9974 Triage.types <> subst_rec_subst_rec thm
R9956:9974 Triage.types <> subst_rec_subst_rec thm
R10019:10019 Coq.Init.Datatypes <> S constr
R10022:10022 Coq.Init.Datatypes <> S constr
R10025:10025 Coq.Init.Datatypes <> S constr
R10039:10041 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10042:10042 Coq.Init.Datatypes <> S constr
R10071:10089 Triage.types <> subst_rec_lift_rec1 thm
R10071:10089 Triage.types <> subst_rec_lift_rec1 thm
R10071:10089 Triage.types <> subst_rec_lift_rec1 thm
R10115:10122 Triage.subtypes <> sub_zero constr
R10175:10175 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10195:10216 Triage.types <> variant_subst_rec_miss thm
R10195:10216 Triage.types <> variant_subst_rec_miss thm
R10195:10216 Triage.types <> variant_subst_rec_miss thm
R10272:10290 Triage.types <> subst_rec_subst_rec thm
R10272:10290 Triage.types <> subst_rec_subst_rec thm
R10272:10290 Triage.types <> subst_rec_subst_rec thm
R10327:10327 Coq.Init.Nat <> ::nat_scope:x_'-'_x not
R10353:10360 Triage.subtypes <> sub_zero constr
R10375:10382 Triage.subtypes <> bffs_aug def
R10385:10392 Triage.subtypes <> bfff_aug def
R10419:10426 Triage.subtypes <> sub_bffs constr
R10419:10426 Triage.subtypes <> sub_bffs constr
R10440:10447 Triage.subtypes <> bffs_aug def
R10450:10457 Triage.subtypes <> bfff_aug def
R10484:10491 Triage.subtypes <> sub_bfff constr
R10484:10491 Triage.subtypes <> sub_bfff constr
prf 10508:10519 <> subtype_lift
binder 10529:10529 <> n:84
binder 10531:10532 <> ty:85
R10535:10541 Triage.subtypes <> subtype ind
R10543:10544 Triage.subtypes <> ty:85 var
R10547:10551 Triage.types <> quant def
R10553:10553 Triage.subtypes <> n:84 var
R10556:10559 Triage.types <> lift def
R10561:10561 Triage.subtypes <> n:84 var
R10563:10564 Triage.subtypes <> ty:85 var
R10624:10627 Triage.types <> lift def
R10638:10650 Triage.types <> lift_rec_null thm
R10638:10650 Triage.types <> lift_rec_null thm
R10638:10650 Triage.types <> lift_rec_null thm
R10674:10674 Coq.Init.Datatypes <> S constr
R10686:10686 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10706:10714 Triage.subtypes <> sub_trans constr
R10734:10741 Triage.subtypes <> sub_lift constr
R10763:10767 Triage.types <> quant def
R10772:10776 Triage.types <> Quant constr
R10779:10782 Triage.types <> lift def
R10786:10786 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10802:10806 Triage.types <> quant def
R10811:10814 Triage.types <> lift def
R10819:10823 Triage.types <> Quant constr
R10826:10829 Triage.types <> lift def
R10880:10883 Triage.types <> lift def
R10901:10917 Triage.types <> lift_rec_lift_rec thm
R10674:10674 Coq.Init.Datatypes <> S constr
R10686:10686 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10706:10714 Triage.subtypes <> sub_trans constr
R10734:10741 Triage.subtypes <> sub_lift constr
R10763:10767 Triage.types <> quant def
R10772:10776 Triage.types <> Quant constr
R10779:10782 Triage.types <> lift def
R10786:10786 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R10802:10806 Triage.types <> quant def
R10811:10814 Triage.types <> lift def
R10819:10823 Triage.types <> Quant constr
R10826:10829 Triage.types <> lift def
R10901:10917 Triage.types <> lift_rec_lift_rec thm
R10901:10917 Triage.types <> lift_rec_lift_rec thm
R10901:10917 Triage.types <> lift_rec_lift_rec thm
R10901:10917 Triage.types <> lift_rec_lift_rec thm
prf 10965:10977 <> subtype_lift2
binder 10988:10988 <> n:86
binder 10990:10991 <> ty:87
R10994:11000 Triage.subtypes <> subtype ind
R11003:11007 Triage.types <> quant def
R11009:11009 Triage.subtypes <> n:86 var
R11012:11015 Triage.types <> lift def
R11017:11017 Triage.subtypes <> n:86 var
R11019:11020 Triage.subtypes <> ty:87 var
R11024:11025 Triage.subtypes <> ty:87 var
R11069:11072 Triage.types <> lift def
R11083:11095 Triage.types <> lift_rec_null thm
R11111:11118 Triage.subtypes <> sub_zero constr
R11083:11095 Triage.types <> lift_rec_null thm
R11083:11095 Triage.types <> lift_rec_null thm
R11111:11118 Triage.subtypes <> sub_zero constr
R11133:11136 Triage.types <> lift def
R11155:11155 Coq.Init.Datatypes <> S constr
R11167:11167 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R11191:11207 Triage.types <> lift_rec_lift_rec thm
R11155:11155 Coq.Init.Datatypes <> S constr
R11167:11167 Coq.Init.Nat <> ::nat_scope:x_'+'_x not
R11191:11207 Triage.types <> lift_rec_lift_rec thm
R11191:11207 Triage.types <> lift_rec_lift_rec thm
R11191:11207 Triage.types <> lift_rec_lift_rec thm
R11191:11207 Triage.types <> lift_rec_lift_rec thm
R11244:11252 Triage.subtypes <> sub_trans constr
R11264:11276 Triage.subtypes <> subtype_quant thm
R11286:11293 Triage.subtypes <> sub_inst constr
R11314:11318 Triage.types <> subst def
R11329:11346 Triage.types <> subst_rec_lift_rec thm
R11244:11252 Triage.subtypes <> sub_trans constr
R11264:11276 Triage.subtypes <> subtype_quant thm
R11286:11293 Triage.subtypes <> sub_inst constr
R11329:11346 Triage.types <> subst_rec_lift_rec thm
R11329:11346 Triage.types <> subst_rec_lift_rec thm
R11329:11346 Triage.types <> subst_rec_lift_rec thm
R11329:11346 Triage.types <> subst_rec_lift_rec thm
R11372:11384 Triage.types <> lift_rec_null thm
R11372:11384 Triage.types <> lift_rec_null thm
R11372:11384 Triage.types <> lift_rec_null thm
R11440:11443 Triage.types <> Leaf constr
R11440:11443 Triage.types <> Leaf constr
prf 11459:11471 <> subtype_lift3
R11486:11488 Coq.Init.Datatypes <> nat ind
binder 11482:11482 <> n:88
R11497:11501 Triage.types <> dtype ind
binder 11492:11493 <> ty:89
R11505:11511 Triage.subtypes <> subtype ind
R11514:11517 Triage.types <> lift def
R11519:11519 Triage.subtypes <> n:88 var