-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathoperator_types.glob
2205 lines (2205 loc) · 92.4 KB
/
operator_types.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 7108832576e8d6e4234b956d45fa5e91
Foperator_types
R1990:1994 Coq.Arith.Arith <> <> lib
R2012:2015 Coq.Bool.Bool <> <> lib
R2033:2036 Coq.Lists.List <> <> lib
R2054:2060 General <> <> lib
R2078:2080 Coq.Arith.Max <> <> lib
R2099:2102 Test <> <> lib
R2120:2130 LamSF_Terms <> <> lib
R2148:2160 LamSF_Tactics <> <> lib
R2178:2200 LamSF_Substitution_term <> <> lib
R2218:2227 Components <> <> lib
R2245:2253 Compounds <> <> lib
R2271:2285 LamSF_reduction <> <> lib
R2303:2314 LamSF_Closed <> <> lib
R2332:2346 type_derivation <> <> lib
R2364:2383 type_derivation_resi <> <> lib
R2401:2419 type_derivation_rwf <> <> lib
R2471:2480 LamSF_Tactics <> multi_step ind
R2493:2495 LamSF_Terms <> Abs constr
R2482:2490 type_derivation <> instance1 ind
R2471:2480 LamSF_Tactics <> multi_step ind
R2493:2495 LamSF_Terms <> Abs constr
R2482:2490 type_derivation <> instance1 ind
R2534:2538 LamSF_Terms <> subst def
R2519:2526 LamSF_Tactics <> succ_red constr
R2649:2652 Coq.Init.Datatypes <> cons constr
R2649:2652 Coq.Init.Datatypes <> cons constr
R2701:2703 Coq.Init.Datatypes <> nil constr
R2701:2703 Coq.Init.Datatypes <> nil constr
R2747:2750 LamSF_Terms <> lift def
R2915:2916 type_derivation <> wf ind
R2919:2921 LamSF_Terms <> Abs constr
R2915:2916 type_derivation <> wf ind
R2919:2921 LamSF_Terms <> Abs constr
prf 2974:2991 <> instance_abs_to_wf
R3071:3077 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3080:3081 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3088:3091 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3082:3084 type_derivation <> wfs ind
R3086:3087 operator_types <> ty var
R3092:3099 type_derivation <> instance def
R3115:3117 operator_types <> ty2 var
R3101:3105 LamSF_Terms <> subst def
R3110:3112 operator_types <> ty0 var
R3107:3108 operator_types <> ty var
R3057:3059 Coq.Init.Logic <> :type_scope:x_'='_x not
R3054:3056 operator_types <> ty1 var
R3060:3062 LamSF_Terms <> Abs constr
R3064:3066 operator_types <> ty0 var
R3031:3032 type_derivation <> wf ind
R3034:3036 operator_types <> ty2 var
R3011:3018 type_derivation <> instance def
R3024:3026 operator_types <> ty2 var
R3020:3022 operator_types <> ty1 var
R3237:3243 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3246:3247 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3254:3257 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3248:3250 type_derivation <> wfs ind
R3252:3253 operator_types <> ty var
R3258:3265 type_derivation <> instance def
R3281:3283 operator_types <> ty2 var
R3267:3271 LamSF_Terms <> subst def
R3276:3278 operator_types <> ty0 var
R3273:3274 operator_types <> ty var
R3223:3225 Coq.Init.Logic <> :type_scope:x_'='_x not
R3220:3222 operator_types <> ty1 var
R3226:3228 LamSF_Terms <> Abs constr
R3230:3232 operator_types <> ty0 var
R3197:3198 type_derivation <> wf ind
R3200:3202 operator_types <> ty2 var
R3181:3183 Coq.Init.Logic <> :type_scope:x_'='_x not
R3178:3180 operator_types <> red var
R3184:3192 type_derivation <> instance1 ind
R3152:3161 LamSF_Tactics <> multi_step ind
R3171:3173 operator_types <> ty2 var
R3167:3169 operator_types <> ty1 var
R3163:3165 operator_types <> red var
R3237:3243 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3246:3247 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3254:3257 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3248:3250 type_derivation <> wfs ind
R3252:3253 operator_types <> ty var
R3258:3265 type_derivation <> instance def
R3281:3283 operator_types <> ty2 var
R3267:3271 LamSF_Terms <> subst def
R3276:3278 operator_types <> ty0 var
R3273:3274 operator_types <> ty var
R3223:3225 Coq.Init.Logic <> :type_scope:x_'='_x not
R3220:3222 operator_types <> ty1 var
R3226:3228 LamSF_Terms <> Abs constr
R3230:3232 operator_types <> ty0 var
R3197:3198 type_derivation <> wf ind
R3200:3202 operator_types <> ty2 var
R3181:3183 Coq.Init.Logic <> :type_scope:x_'='_x not
R3178:3180 operator_types <> red var
R3184:3192 type_derivation <> instance1 ind
R3152:3161 LamSF_Tactics <> multi_step ind
R3171:3173 operator_types <> ty2 var
R3167:3169 operator_types <> ty1 var
R3163:3165 operator_types <> red var
R3382:3383 type_derivation <> wf ind
R3382:3383 type_derivation <> wf ind
R3425:3431 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3442:3443 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3437:3441 LamSF_Terms <> lamSF ind
R3450:3453 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3444:3446 type_derivation <> wfs ind
R3448:3449 operator_types <> ty var
R3454:3461 type_derivation <> instance def
R3464:3468 LamSF_Terms <> subst def
R3470:3471 operator_types <> ty var
R3425:3431 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3442:3443 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3437:3441 LamSF_Terms <> lamSF ind
R3450:3453 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3444:3446 type_derivation <> wfs ind
R3448:3449 operator_types <> ty var
R3454:3461 type_derivation <> instance def
R3464:3468 LamSF_Terms <> subst def
R3470:3471 operator_types <> ty var
R3527:3540 LamSF_Tactics <> transitive_red thm
R3527:3540 LamSF_Tactics <> transitive_red thm
R3566:3570 LamSF_Terms <> subst def
R3581:3608 type_derivation <> subst_rec_preserves_instance thm
prf 3640:3663 <> instance_preserves_funty
R3748:3754 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3764:3765 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3787:3790 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3769:3771 Coq.Init.Logic <> :type_scope:x_'='_x not
R3766:3768 operator_types <> ty2 var
R3772:3776 type_derivation <> funty def
R3783:3786 operator_types <> ty22 var
R3778:3781 operator_types <> ty21 var
R3809:3812 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3791:3798 type_derivation <> instance def
R3805:3808 operator_types <> ty11 var
R3800:3803 operator_types <> ty21 var
R3813:3820 type_derivation <> instance def
R3827:3830 operator_types <> ty22 var
R3822:3825 operator_types <> ty12 var
R3725:3727 Coq.Init.Logic <> :type_scope:x_'='_x not
R3722:3724 operator_types <> ty1 var
R3728:3732 type_derivation <> funty def
R3739:3742 operator_types <> ty12 var
R3734:3737 operator_types <> ty11 var
R3683:3690 type_derivation <> instance def
R3696:3698 operator_types <> ty2 var
R3692:3694 operator_types <> ty1 var
R3954:3960 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3970:3971 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3993:3996 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3975:3977 Coq.Init.Logic <> :type_scope:x_'='_x not
R3972:3974 operator_types <> ty2 var
R3978:3982 type_derivation <> funty def
R3989:3992 operator_types <> ty22 var
R3984:3987 operator_types <> ty21 var
R4015:4018 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3997:4004 type_derivation <> instance def
R4011:4014 operator_types <> ty11 var
R4006:4009 operator_types <> ty21 var
R4019:4026 type_derivation <> instance def
R4033:4036 operator_types <> ty22 var
R4028:4031 operator_types <> ty12 var
R3931:3933 Coq.Init.Logic <> :type_scope:x_'='_x not
R3928:3930 operator_types <> ty1 var
R3934:3938 type_derivation <> funty def
R3945:3948 operator_types <> ty12 var
R3940:3943 operator_types <> ty11 var
R3893:3895 Coq.Init.Logic <> :type_scope:x_'='_x not
R3890:3892 operator_types <> red var
R3896:3904 type_derivation <> instance1 ind
R3864:3873 LamSF_Tactics <> multi_step ind
R3883:3885 operator_types <> ty2 var
R3879:3881 operator_types <> ty1 var
R3875:3877 operator_types <> red var
R3954:3960 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3970:3971 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R3993:3996 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3975:3977 Coq.Init.Logic <> :type_scope:x_'='_x not
R3972:3974 operator_types <> ty2 var
R3978:3982 type_derivation <> funty def
R3989:3992 operator_types <> ty22 var
R3984:3987 operator_types <> ty21 var
R4015:4018 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R3997:4004 type_derivation <> instance def
R4011:4014 operator_types <> ty11 var
R4006:4009 operator_types <> ty21 var
R4019:4026 type_derivation <> instance def
R4033:4036 operator_types <> ty22 var
R4028:4031 operator_types <> ty12 var
R3931:3933 Coq.Init.Logic <> :type_scope:x_'='_x not
R3928:3930 operator_types <> ty1 var
R3934:3938 type_derivation <> funty def
R3945:3948 operator_types <> ty12 var
R3940:3943 operator_types <> ty11 var
R3893:3895 Coq.Init.Logic <> :type_scope:x_'='_x not
R3890:3892 operator_types <> red var
R3896:3904 type_derivation <> instance1 ind
R3864:3873 LamSF_Tactics <> multi_step ind
R3883:3885 operator_types <> ty2 var
R3879:3881 operator_types <> ty1 var
R3875:3877 operator_types <> red var
R4135:4136 type_derivation <> wf ind
R4135:4136 type_derivation <> wf ind
R4188:4195 LamSF_Tactics <> zero_red constr
R4188:4195 LamSF_Tactics <> zero_red constr
R4235:4241 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4259:4260 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4254:4258 LamSF_Terms <> lamSF ind
R4280:4283 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4262:4264 Coq.Init.Logic <> :type_scope:x_'='_x not
R4265:4269 type_derivation <> funty def
R4276:4279 operator_types <> ty22 var
R4271:4274 operator_types <> ty21 var
R4302:4305 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4284:4291 type_derivation <> instance def
R4293:4296 operator_types <> ty21 var
R4306:4313 type_derivation <> instance def
R4319:4322 operator_types <> ty22 var
R4235:4241 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4259:4260 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4254:4258 LamSF_Terms <> lamSF ind
R4280:4283 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4262:4264 Coq.Init.Logic <> :type_scope:x_'='_x not
R4265:4269 type_derivation <> funty def
R4276:4279 operator_types <> ty22 var
R4271:4274 operator_types <> ty21 var
R4302:4305 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4284:4291 type_derivation <> instance def
R4293:4296 operator_types <> ty21 var
R4306:4313 type_derivation <> instance def
R4319:4322 operator_types <> ty22 var
R4390:4397 LamSF_Tactics <> succ_red constr
R4409:4415 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4433:4434 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4428:4432 LamSF_Terms <> lamSF ind
R4454:4457 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4436:4438 Coq.Init.Logic <> :type_scope:x_'='_x not
R4439:4443 type_derivation <> funty def
R4450:4453 operator_types <> ty22 var
R4445:4448 operator_types <> ty21 var
R4475:4478 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4458:4465 type_derivation <> instance def
R4467:4470 operator_types <> ty21 var
R4479:4486 type_derivation <> instance def
R4493:4496 operator_types <> ty22 var
R4409:4415 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4433:4434 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4428:4432 LamSF_Terms <> lamSF ind
R4454:4457 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4436:4438 Coq.Init.Logic <> :type_scope:x_'='_x not
R4439:4443 type_derivation <> funty def
R4450:4453 operator_types <> ty22 var
R4445:4448 operator_types <> ty21 var
R4475:4478 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4458:4465 type_derivation <> instance def
R4467:4470 operator_types <> ty21 var
R4479:4486 type_derivation <> instance def
R4493:4496 operator_types <> ty22 var
R4564:4577 LamSF_Tactics <> transitive_red thm
R4564:4577 LamSF_Tactics <> transitive_red thm
R4635:4639 type_derivation <> funty def
R4642:4645 Components <> s_op def
R4677:4684 type_derivation <> instance def
R4687:4689 LamSF_Terms <> Abs constr
R4677:4684 type_derivation <> instance def
R4687:4689 LamSF_Terms <> Abs constr
R4867:4874 type_derivation <> instance def
R4877:4879 LamSF_Terms <> App constr
R4882:4884 LamSF_Terms <> App constr
R4887:4888 LamSF_Terms <> Op constr
R4890:4892 LamSF_Terms <> Sop constr
R4867:4874 type_derivation <> instance def
R4877:4879 LamSF_Terms <> App constr
R4882:4884 LamSF_Terms <> App constr
R4887:4888 LamSF_Terms <> Op constr
R4890:4892 LamSF_Terms <> Sop constr
R4977:4983 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4993:4994 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5016:5019 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4998:5000 Coq.Init.Logic <> :type_scope:x_'='_x not
R5001:5005 type_derivation <> funty def
R5012:5015 operator_types <> ty22 var
R5007:5010 operator_types <> ty21 var
R5037:5040 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5020:5027 type_derivation <> instance def
R5029:5032 operator_types <> ty21 var
R5041:5048 type_derivation <> instance def
R5055:5058 operator_types <> ty22 var
R5147:5151 LamSF_Terms <> subst def
R4718:4724 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4727:4728 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R4735:4738 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R4729:4731 type_derivation <> wfs ind
R4733:4734 operator_types <> ty var
R4739:4746 type_derivation <> instance def
R4749:4753 LamSF_Terms <> subst def
R4755:4756 operator_types <> ty var
R4827:4831 LamSF_Terms <> subst def
prf 5207:5216 <> instance_S
R5274:5281 type_derivation <> instance def
R5298:5302 type_derivation <> funty def
R5333:5337 type_derivation <> funty def
R5356:5360 type_derivation <> funty def
R5366:5368 operator_types <> ty3 var
R5362:5364 operator_types <> ty1 var
R5340:5344 type_derivation <> funty def
R5350:5352 operator_types <> ty2 var
R5346:5348 operator_types <> ty1 var
R5305:5309 type_derivation <> funty def
R5316:5320 type_derivation <> funty def
R5326:5328 operator_types <> ty3 var
R5322:5324 operator_types <> ty2 var
R5311:5313 operator_types <> ty1 var
R5284:5287 type_derivation <> opty def
R5289:5291 LamSF_Terms <> Sop constr
R5263:5265 type_derivation <> wfs ind
R5267:5269 operator_types <> ty3 var
R5252:5254 type_derivation <> wfs ind
R5256:5258 operator_types <> ty2 var
R5241:5243 type_derivation <> wfs ind
R5245:5247 operator_types <> ty1 var
R5390:5397 type_derivation <> instance def
R5435:5438 Coq.Init.Datatypes <> cons constr
R5445:5448 Coq.Init.Datatypes <> cons constr
R5455:5458 Coq.Init.Datatypes <> cons constr
R5464:5466 Coq.Init.Datatypes <> nil constr
R5435:5438 Coq.Init.Datatypes <> cons constr
R5445:5448 Coq.Init.Datatypes <> cons constr
R5455:5458 Coq.Init.Datatypes <> cons constr
R5464:5466 Coq.Init.Datatypes <> nil constr
prf 5484:5491 <> derive_S
R5569:5578 type_derivation <> derivation ind
R5595:5599 type_derivation <> funty def
R5630:5634 type_derivation <> funty def
R5653:5657 type_derivation <> funty def
R5663:5665 operator_types <> ty3 var
R5659:5661 operator_types <> ty1 var
R5637:5641 type_derivation <> funty def
R5647:5649 operator_types <> ty2 var
R5643:5645 operator_types <> ty1 var
R5602:5606 type_derivation <> funty def
R5613:5617 type_derivation <> funty def
R5623:5625 operator_types <> ty3 var
R5619:5621 operator_types <> ty2 var
R5608:5610 operator_types <> ty1 var
R5586:5589 Components <> s_op def
R5580:5584 operator_types <> gamma var
R5557:5559 type_derivation <> wfs ind
R5561:5563 operator_types <> ty3 var
R5546:5548 type_derivation <> wfs ind
R5550:5552 operator_types <> ty2 var
R5535:5537 type_derivation <> wfs ind
R5539:5541 operator_types <> ty1 var
R5522:5524 type_derivation <> wfc ind
R5526:5530 operator_types <> gamma var
R5695:5709 type_derivation <> derive_instance thm
R5720:5728 type_derivation <> derive_op constr
R5739:5748 operator_types <> instance_S thm
prf 5765:5775 <> instance_S2
R5826:5833 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5864:5867 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R5859:5863 LamSF_Terms <> lamSF ind
R5909:5913 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5870:5872 Coq.Init.Logic <> :type_scope:x_'='_x not
R5868:5869 operator_types <> ty var
R5873:5877 type_derivation <> funty def
R5884:5888 type_derivation <> funty def
R5895:5899 type_derivation <> funty def
R5905:5906 operator_types <> x8 var
R5901:5903 operator_types <> ty2 var
R5890:5892 operator_types <> ty0 var
R5879:5881 operator_types <> ty1 var
R5929:5933 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5914:5921 type_derivation <> instance def
R5927:5928 operator_types <> x7 var
R5923:5925 operator_types <> ty2 var
R5960:5964 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5934:5941 type_derivation <> instance def
R5948:5952 type_derivation <> funty def
R5957:5958 operator_types <> x0 var
R5954:5955 operator_types <> x7 var
R5943:5945 operator_types <> ty0 var
R6002:6006 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R5965:5972 type_derivation <> instance def
R5979:5983 type_derivation <> funty def
R5989:5993 type_derivation <> funty def
R5998:5999 operator_types <> x1 var
R5995:5996 operator_types <> x0 var
R5985:5986 operator_types <> x7 var
R5974:5976 operator_types <> ty1 var
R6007:6014 type_derivation <> instance def
R6019:6020 operator_types <> x8 var
R6016:6017 operator_types <> x1 var
R5816:5817 type_derivation <> wf ind
R5819:5820 operator_types <> ty var
R5791:5798 type_derivation <> instance def
R5810:5811 operator_types <> ty var
R5800:5803 type_derivation <> opty def
R5805:5807 LamSF_Terms <> Sop constr
R6039:6042 type_derivation <> opty def
R6045:6049 type_derivation <> quant def
R6052:6056 type_derivation <> funty def
R6077:6081 type_derivation <> funty def
prf 6238:6249 <> derive_rwf_S
R6304:6311 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6342:6345 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6337:6341 LamSF_Terms <> lamSF ind
R6387:6391 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6348:6350 Coq.Init.Logic <> :type_scope:x_'='_x not
R6346:6347 operator_types <> ty var
R6351:6355 type_derivation <> funty def
R6362:6366 type_derivation <> funty def
R6373:6377 type_derivation <> funty def
R6383:6384 operator_types <> x8 var
R6379:6381 operator_types <> ty2 var
R6368:6370 operator_types <> ty0 var
R6357:6359 operator_types <> ty1 var
R6407:6411 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6392:6399 type_derivation <> instance def
R6405:6406 operator_types <> x7 var
R6401:6403 operator_types <> ty2 var
R6438:6442 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6412:6419 type_derivation <> instance def
R6426:6430 type_derivation <> funty def
R6435:6436 operator_types <> x0 var
R6432:6433 operator_types <> x7 var
R6421:6423 operator_types <> ty0 var
R6480:6484 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6443:6450 type_derivation <> instance def
R6457:6461 type_derivation <> funty def
R6467:6471 type_derivation <> funty def
R6476:6477 operator_types <> x1 var
R6473:6474 operator_types <> x0 var
R6463:6464 operator_types <> x7 var
R6452:6454 operator_types <> ty1 var
R6485:6492 type_derivation <> instance def
R6497:6498 operator_types <> x8 var
R6494:6495 operator_types <> x1 var
R6271:6284 type_derivation_rwf <> derivation_rwf ind
R6297:6298 operator_types <> ty var
R6292:6295 Components <> s_op def
R6286:6290 operator_types <> gamma var
R6549:6559 operator_types <> instance_S2 thm
prf 6576:6585 <> instance_A
R6629:6636 type_derivation <> instance def
R6650:6654 type_derivation <> funty def
R6674:6678 type_derivation <> funty def
R6684:6686 operator_types <> ty2 var
R6680:6682 operator_types <> ty1 var
R6657:6661 type_derivation <> funty def
R6667:6669 operator_types <> ty2 var
R6663:6665 operator_types <> ty1 var
R6639:6642 type_derivation <> opty def
R6644:6646 LamSF_Terms <> Aop constr
R6617:6619 type_derivation <> wfs ind
R6621:6623 operator_types <> ty2 var
R6606:6608 type_derivation <> wfs ind
R6610:6612 operator_types <> ty1 var
R6705:6712 type_derivation <> instance def
R6752:6755 Coq.Init.Datatypes <> cons constr
R6762:6765 Coq.Init.Datatypes <> cons constr
R6771:6773 Coq.Init.Datatypes <> nil constr
R6752:6755 Coq.Init.Datatypes <> cons constr
R6762:6765 Coq.Init.Datatypes <> cons constr
R6771:6773 Coq.Init.Datatypes <> nil constr
prf 6790:6797 <> derive_A
R6859:6868 type_derivation <> derivation ind
R6883:6887 type_derivation <> funty def
R6907:6911 type_derivation <> funty def
R6917:6919 operator_types <> ty2 var
R6913:6915 operator_types <> ty1 var
R6890:6894 type_derivation <> funty def
R6900:6902 operator_types <> ty2 var
R6896:6898 operator_types <> ty1 var
R6876:6879 Components <> a_op def
R6870:6874 operator_types <> gamma var
R6847:6849 type_derivation <> wfs ind
R6851:6853 operator_types <> ty2 var
R6836:6838 type_derivation <> wfs ind
R6840:6842 operator_types <> ty1 var
R6823:6825 type_derivation <> wfc ind
R6827:6831 operator_types <> gamma var
R6947:6961 type_derivation <> derive_instance thm
R6972:6980 type_derivation <> derive_op constr
R6991:7000 operator_types <> instance_A thm
prf 7016:7026 <> instance_A2
R7077:7083 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7095:7096 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7127:7130 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R7099:7101 Coq.Init.Logic <> :type_scope:x_'='_x not
R7097:7098 operator_types <> ty var
R7102:7106 type_derivation <> funty def
R7113:7117 type_derivation <> funty def
R7123:7125 operator_types <> ty3 var
R7119:7121 operator_types <> ty2 var
R7108:7110 operator_types <> ty1 var
R7131:7138 type_derivation <> instance def
R7145:7149 type_derivation <> funty def
R7155:7157 operator_types <> ty3 var
R7151:7153 operator_types <> ty2 var
R7140:7142 operator_types <> ty1 var
R7067:7068 type_derivation <> wf ind
R7070:7071 operator_types <> ty var
R7042:7049 type_derivation <> instance def
R7061:7062 operator_types <> ty var
R7051:7054 type_derivation <> opty def
R7056:7058 LamSF_Terms <> Aop constr
R7176:7179 type_derivation <> opty def
R7182:7186 type_derivation <> quant def
R7300:7312 LamSF_Substitution_term <> lift_rec_null thm
R7300:7312 LamSF_Substitution_term <> lift_rec_null thm
R7323:7340 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7323:7340 LamSF_Substitution_term <> subst_rec_lift_rec thm
R7363:7375 LamSF_Substitution_term <> lift_rec_null thm
R7363:7375 LamSF_Substitution_term <> lift_rec_null thm
R7434:7447 LamSF_Tactics <> transitive_red thm
R7459:7482 type_derivation <> preserves_funty_instance thm
prf 7500:7509 <> instance_K
R7552:7559 type_derivation <> instance def
R7573:7577 type_derivation <> funty def
R7584:7588 type_derivation <> funty def
R7594:7596 operator_types <> ty1 var
R7590:7592 operator_types <> ty2 var
R7579:7581 operator_types <> ty1 var
R7562:7565 type_derivation <> opty def
R7567:7569 LamSF_Terms <> Kop constr
R7541:7543 type_derivation <> wfs ind
R7545:7547 operator_types <> ty2 var
R7530:7532 type_derivation <> wfs ind
R7534:7536 operator_types <> ty1 var
R7615:7622 type_derivation <> instance def
R7660:7663 Coq.Init.Datatypes <> cons constr
R7670:7673 Coq.Init.Datatypes <> cons constr
R7679:7681 Coq.Init.Datatypes <> nil constr
R7660:7663 Coq.Init.Datatypes <> cons constr
R7670:7673 Coq.Init.Datatypes <> cons constr
R7679:7681 Coq.Init.Datatypes <> nil constr
prf 7698:7705 <> derive_K
R7768:7777 type_derivation <> derivation ind
R7791:7795 type_derivation <> funty def
R7802:7806 type_derivation <> funty def
R7812:7814 operator_types <> ty1 var
R7808:7810 operator_types <> ty2 var
R7797:7799 operator_types <> ty1 var
R7785:7788 Components <> k_op def
R7779:7783 operator_types <> gamma var
R7755:7757 type_derivation <> wfs ind
R7759:7761 operator_types <> ty2 var
R7744:7746 type_derivation <> wfs ind
R7748:7750 operator_types <> ty1 var
R7731:7733 type_derivation <> wfc ind
R7735:7739 operator_types <> gamma var
R7843:7857 type_derivation <> derive_instance thm
R7868:7876 type_derivation <> derive_op constr
R7887:7896 operator_types <> instance_K thm
prf 7912:7922 <> instance_K2
R7973:7979 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R7991:7992 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8023:8026 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R7995:7997 Coq.Init.Logic <> :type_scope:x_'='_x not
R7993:7994 operator_types <> ty var
R7998:8002 type_derivation <> funty def
R8009:8013 type_derivation <> funty def
R8019:8021 operator_types <> ty3 var
R8015:8017 operator_types <> ty2 var
R8004:8006 operator_types <> ty1 var
R8027:8034 type_derivation <> instance def
R8040:8042 operator_types <> ty3 var
R8036:8038 operator_types <> ty1 var
R7963:7964 type_derivation <> wf ind
R7966:7967 operator_types <> ty var
R7938:7945 type_derivation <> instance def
R7957:7958 operator_types <> ty var
R7947:7950 type_derivation <> opty def
R7952:7954 LamSF_Terms <> Kop constr
R8060:8063 type_derivation <> opty def
R8066:8070 type_derivation <> quant def
R8184:8196 LamSF_Substitution_term <> lift_rec_null thm
R8184:8196 LamSF_Substitution_term <> lift_rec_null thm
R8207:8224 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8207:8224 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8247:8259 LamSF_Substitution_term <> lift_rec_null thm
R8247:8259 LamSF_Substitution_term <> lift_rec_null thm
R8318:8331 LamSF_Tactics <> transitive_red thm
prf 8348:8357 <> instance_E
R8417:8424 type_derivation <> instance def
R8438:8442 type_derivation <> funty def
R8449:8453 type_derivation <> funty def
R8460:8464 type_derivation <> funty def
R8471:8475 type_derivation <> funty def
R8481:8483 operator_types <> ty3 var
R8477:8479 operator_types <> ty3 var
R8466:8468 operator_types <> ty3 var
R8455:8457 operator_types <> ty2 var
R8444:8446 operator_types <> ty1 var
R8427:8430 type_derivation <> opty def
R8432:8434 LamSF_Terms <> Eop constr
R8406:8408 type_derivation <> wfs ind
R8410:8412 operator_types <> ty3 var
R8394:8396 type_derivation <> wfs ind
R8398:8400 operator_types <> ty2 var
R8383:8385 type_derivation <> wfs ind
R8387:8389 operator_types <> ty1 var
R8504:8511 type_derivation <> instance def
R8549:8552 Coq.Init.Datatypes <> cons constr
R8559:8562 Coq.Init.Datatypes <> cons constr
R8569:8572 Coq.Init.Datatypes <> cons constr
R8578:8580 Coq.Init.Datatypes <> nil constr
R8549:8552 Coq.Init.Datatypes <> cons constr
R8559:8562 Coq.Init.Datatypes <> cons constr
R8569:8572 Coq.Init.Datatypes <> cons constr
R8578:8580 Coq.Init.Datatypes <> nil constr
prf 8598:8605 <> derive_E
R8685:8694 type_derivation <> derivation ind
R8708:8712 type_derivation <> funty def
R8719:8723 type_derivation <> funty def
R8730:8734 type_derivation <> funty def
R8741:8745 type_derivation <> funty def
R8751:8753 operator_types <> ty2 var
R8747:8749 operator_types <> ty2 var
R8736:8738 operator_types <> ty2 var
R8725:8727 operator_types <> ty1 var
R8714:8716 operator_types <> ty0 var
R8702:8705 Components <> e_op def
R8696:8700 operator_types <> gamma var
R8671:8673 type_derivation <> wfs ind
R8675:8677 operator_types <> ty2 var
R8660:8662 type_derivation <> wfs ind
R8664:8666 operator_types <> ty1 var
R8649:8651 type_derivation <> wfs ind
R8653:8655 operator_types <> ty0 var
R8635:8637 type_derivation <> wfc ind
R8639:8643 operator_types <> gamma var
R8783:8797 type_derivation <> derive_instance thm
R8808:8816 type_derivation <> derive_op constr
R8827:8836 operator_types <> instance_E thm
prf 8853:8863 <> instance_E2
R8914:8920 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8940:8942 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8950:8953 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8943:8945 type_derivation <> wfs ind
R8947:8949 operator_types <> ty1 var
R8961:8964 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8954:8956 type_derivation <> wfs ind
R8958:8960 operator_types <> ty2 var
R8972:8975 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8965:8967 type_derivation <> wfs ind
R8969:8971 operator_types <> ty3 var
R8983:8986 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8976:8978 type_derivation <> wfs ind
R8980:8982 operator_types <> ty4 var
R8994:8998 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8987:8989 type_derivation <> wfs ind
R8991:8993 operator_types <> ty5 var
R9053:9056 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9001:9003 Coq.Init.Logic <> :type_scope:x_'='_x not
R8999:9000 operator_types <> ty var
R9004:9008 type_derivation <> funty def
R9015:9019 type_derivation <> funty def
R9026:9030 type_derivation <> funty def
R9037:9041 type_derivation <> funty def
R9047:9049 operator_types <> ty5 var
R9043:9045 operator_types <> ty4 var
R9032:9034 operator_types <> ty3 var
R9021:9023 operator_types <> ty2 var
R9010:9012 operator_types <> ty1 var
R9073:9076 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9057:9064 type_derivation <> instance def
R9070:9072 operator_types <> ty5 var
R9066:9068 operator_types <> ty3 var
R9077:9084 type_derivation <> instance def
R9090:9092 operator_types <> ty5 var
R9086:9088 operator_types <> ty4 var
R8904:8905 type_derivation <> wf ind
R8907:8908 operator_types <> ty var
R8879:8886 type_derivation <> instance def
R8898:8899 operator_types <> ty var
R8888:8891 type_derivation <> opty def
R8893:8895 LamSF_Terms <> Eop constr
R9110:9113 type_derivation <> opty def
R9116:9120 type_derivation <> quant def
R9261:9280 type_derivation <> instance_implies_wfs thm
R9261:9280 type_derivation <> instance_implies_wfs thm
R9261:9280 type_derivation <> instance_implies_wfs thm
R9261:9280 type_derivation <> instance_implies_wfs thm
R9314:9327 type_derivation <> wf_implies_wfs thm
R9339:9352 LamSF_Tactics <> transitive_red thm
R9363:9376 LamSF_Tactics <> transitive_red thm
prf 9393:9404 <> derive_rwf_E
R9459:9465 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R9485:9487 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R9495:9498 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9488:9490 type_derivation <> wfs ind
R9492:9494 operator_types <> ty1 var
R9506:9509 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9499:9501 type_derivation <> wfs ind
R9503:9505 operator_types <> ty2 var
R9517:9520 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9510:9512 type_derivation <> wfs ind
R9514:9516 operator_types <> ty3 var
R9528:9531 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9521:9523 type_derivation <> wfs ind
R9525:9527 operator_types <> ty4 var
R9539:9543 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9532:9534 type_derivation <> wfs ind
R9536:9538 operator_types <> ty5 var
R9598:9601 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9546:9548 Coq.Init.Logic <> :type_scope:x_'='_x not
R9544:9545 operator_types <> ty var
R9549:9553 type_derivation <> funty def
R9560:9564 type_derivation <> funty def
R9571:9575 type_derivation <> funty def
R9582:9586 type_derivation <> funty def
R9592:9594 operator_types <> ty5 var
R9588:9590 operator_types <> ty4 var
R9577:9579 operator_types <> ty3 var
R9566:9568 operator_types <> ty2 var
R9555:9557 operator_types <> ty1 var
R9618:9621 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R9602:9609 type_derivation <> instance def
R9615:9617 operator_types <> ty5 var
R9611:9613 operator_types <> ty3 var
R9622:9629 type_derivation <> instance def
R9635:9637 operator_types <> ty5 var
R9631:9633 operator_types <> ty4 var
R9426:9439 type_derivation_rwf <> derivation_rwf ind
R9452:9453 operator_types <> ty var
R9447:9450 Components <> e_op def
R9441:9445 operator_types <> gamma var
R9686:9696 operator_types <> instance_E2 thm
prf 9712:9721 <> instance_G
R9765:9772 type_derivation <> instance def
R9805:9809 type_derivation <> funty def
R9887:9891 type_derivation <> funty def
R9898:9900 operator_types <> ty2 var
R9893:9895 operator_types <> ty1 var
R9812:9814 LamSF_Terms <> Abs constr
R9817:9821 type_derivation <> funty def
R9855:9859 type_derivation <> funty def
R9872:9875 LamSF_Terms <> lift def
R9879:9881 operator_types <> ty2 var
R9862:9866 type_derivation <> varty def
R9824:9828 type_derivation <> funty def
R9841:9844 LamSF_Terms <> lift def
R9848:9850 operator_types <> ty1 var
R9831:9835 type_derivation <> varty def
R9775:9778 type_derivation <> opty def
R9780:9782 LamSF_Terms <> Gop constr
R9753:9755 type_derivation <> wfs ind
R9757:9759 operator_types <> ty2 var
R9742:9744 type_derivation <> wfs ind
R9746:9748 operator_types <> ty1 var
R9919:9926 type_derivation <> instance def
R9964:9967 Coq.Init.Datatypes <> cons constr
R9974:9977 Coq.Init.Datatypes <> cons constr
R9983:9985 Coq.Init.Datatypes <> nil constr
R9964:9967 Coq.Init.Datatypes <> cons constr
R9974:9977 Coq.Init.Datatypes <> cons constr
R9983:9985 Coq.Init.Datatypes <> nil constr
prf 10002:10009 <> derive_G
R10073:10082 type_derivation <> derivation ind
R10096:10100 type_derivation <> funty def
R10179:10183 type_derivation <> funty def
R10189:10191 operator_types <> ty2 var
R10185:10187 operator_types <> ty1 var
R10103:10105 LamSF_Terms <> Abs constr
R10108:10112 type_derivation <> funty def
R10146:10150 type_derivation <> funty def
R10163:10166 LamSF_Terms <> lift def
R10170:10172 operator_types <> ty2 var
R10153:10157 type_derivation <> varty def
R10115:10119 type_derivation <> funty def
R10132:10135 LamSF_Terms <> lift def
R10139:10141 operator_types <> ty1 var
R10122:10126 type_derivation <> varty def
R10090:10093 Components <> g_op def
R10084:10088 operator_types <> gamma var
R10060:10062 type_derivation <> wfs ind
R10064:10066 operator_types <> ty2 var
R10049:10051 type_derivation <> wfs ind
R10053:10055 operator_types <> ty1 var
R10036:10038 type_derivation <> wfc ind
R10040:10044 operator_types <> gamma var
R10221:10235 type_derivation <> derive_instance thm
R10246:10254 type_derivation <> derive_op constr
R10265:10274 operator_types <> instance_G thm
prf 10289:10299 <> instance_G2
R10350:10356 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10368:10369 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10400:10404 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R10372:10374 Coq.Init.Logic <> :type_scope:x_'='_x not
R10370:10371 operator_types <> ty var
R10375:10379 type_derivation <> funty def
R10386:10390 type_derivation <> funty def
R10396:10398 operator_types <> ty3 var
R10392:10394 operator_types <> ty2 var
R10381:10383 operator_types <> ty1 var
R10405:10412 type_derivation <> instance def
R10419:10421 LamSF_Terms <> Abs constr
R10424:10428 type_derivation <> funty def
R10462:10466 type_derivation <> funty def
R10479:10482 LamSF_Terms <> lift def
R10486:10488 operator_types <> ty3 var
R10469:10473 type_derivation <> varty def
R10431:10435 type_derivation <> funty def
R10448:10451 LamSF_Terms <> lift def
R10455:10457 operator_types <> ty2 var
R10438:10442 type_derivation <> varty def
R10414:10416 operator_types <> ty1 var
R10340:10341 type_derivation <> wf ind
R10343:10344 operator_types <> ty var
R10315:10322 type_derivation <> instance def
R10334:10335 operator_types <> ty var
R10324:10327 type_derivation <> opty def
R10329:10331 LamSF_Terms <> Gop constr
R10511:10514 type_derivation <> opty def
R10517:10521 type_derivation <> quant def
R10611:10618 type_derivation <> instance def
R10621:10623 LamSF_Terms <> App constr
R10626:10628 LamSF_Terms <> App constr
R10631:10632 LamSF_Terms <> Op constr
R10634:10636 LamSF_Terms <> Sop constr
R10611:10618 type_derivation <> instance def
R10621:10623 LamSF_Terms <> App constr
R10626:10628 LamSF_Terms <> App constr
R10631:10632 LamSF_Terms <> Op constr
R10634:10636 LamSF_Terms <> Sop constr
R10723:10729 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10739:10740 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10762:10765 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R10744:10746 Coq.Init.Logic <> :type_scope:x_'='_x not
R10747:10751 type_derivation <> funty def
R10758:10761 operator_types <> ty22 var
R10753:10756 operator_types <> ty21 var
R10784:10787 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R10766:10773 type_derivation <> instance def
R10775:10778 operator_types <> ty21 var
R10788:10795 type_derivation <> instance def
R10803:10806 operator_types <> ty22 var
R10723:10729 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10739:10740 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10762:10765 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R10744:10746 Coq.Init.Logic <> :type_scope:x_'='_x not
R10747:10751 type_derivation <> funty def
R10758:10761 operator_types <> ty22 var
R10753:10756 operator_types <> ty21 var
R10784:10787 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R10766:10773 type_derivation <> instance def
R10775:10778 operator_types <> ty21 var
R10788:10795 type_derivation <> instance def
R10803:10806 operator_types <> ty22 var
R10823:10846 operator_types <> instance_preserves_funty thm
R10931:10944 LamSF_Tactics <> transitive_red thm
R10931:10944 LamSF_Tactics <> transitive_red thm
R10967:10990 LamSF_Tactics <> preserves_abs_multi_step thm
R11016:11039 type_derivation <> preserves_funty_instance thm
R11016:11039 type_derivation <> preserves_funty_instance thm
R11051:11059 type_derivation <> wfs_funty constr
R11071:11079 type_derivation <> wfs_funty constr
R11090:11115 type_derivation <> preserves_funty_r_instance thm
R11090:11115 type_derivation <> preserves_funty_r_instance thm
R11127:11133 type_derivation <> wfs_var constr
R11144:11170 type_derivation <> lift_rec_preserves_instance thm
R11181:11206 type_derivation <> preserves_funty_r_instance thm
R11181:11206 type_derivation <> preserves_funty_r_instance thm
R11218:11224 type_derivation <> wfs_var constr
R11235:11261 type_derivation <> lift_rec_preserves_instance thm
prf 11278:11289 <> derive_rwf_G
R11344:11350 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11362:11363 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11394:11398 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R11366:11368 Coq.Init.Logic <> :type_scope:x_'='_x not
R11364:11365 operator_types <> ty var
R11369:11373 type_derivation <> funty def
R11380:11384 type_derivation <> funty def
R11390:11392 operator_types <> ty3 var
R11386:11388 operator_types <> ty2 var
R11375:11377 operator_types <> ty1 var
R11399:11406 type_derivation <> instance def
R11413:11415 LamSF_Terms <> Abs constr
R11418:11422 type_derivation <> funty def
R11456:11460 type_derivation <> funty def
R11473:11476 LamSF_Terms <> lift def
R11480:11482 operator_types <> ty3 var
R11463:11467 type_derivation <> varty def
R11425:11429 type_derivation <> funty def
R11442:11445 LamSF_Terms <> lift def
R11449:11451 operator_types <> ty2 var
R11432:11436 type_derivation <> varty def
R11408:11410 operator_types <> ty1 var
R11311:11324 type_derivation_rwf <> derivation_rwf ind
R11337:11338 operator_types <> ty var
R11332:11335 Components <> g_op def
R11326:11330 operator_types <> gamma var
R11536:11546 operator_types <> instance_G2 thm
prf 11564:11573 <> instance_Q
R11617:11624 type_derivation <> instance def
R11656:11660 type_derivation <> funty def
R11726:11730 type_derivation <> funty def
R11808:11812 type_derivation <> funty def
R11818:11820 operator_types <> ty2 var
R11814:11816 operator_types <> ty1 var
R11738:11742 type_derivation <> funty def
R11749:11753 type_derivation <> funty def
R11759:11761 operator_types <> ty2 var
R11755:11757 operator_types <> ty2 var
R11744:11746 operator_types <> ty2 var
R11663:11665 LamSF_Terms <> Abs constr
R11668:11672 type_derivation <> funty def
R11685:11688 LamSF_Terms <> lift def
R11692:11694 operator_types <> ty2 var
R11675:11679 type_derivation <> varty def
R11627:11630 type_derivation <> opty def
R11632:11634 LamSF_Terms <> Qop constr
R11605:11607 type_derivation <> wfs ind
R11609:11611 operator_types <> ty2 var
R11594:11596 type_derivation <> wfs ind
R11598:11600 operator_types <> ty1 var
R11840:11847 type_derivation <> instance def
R11885:11888 Coq.Init.Datatypes <> cons constr
R11895:11898 Coq.Init.Datatypes <> cons constr
R11904:11906 Coq.Init.Datatypes <> nil constr
R11885:11888 Coq.Init.Datatypes <> cons constr
R11895:11898 Coq.Init.Datatypes <> cons constr
R11904:11906 Coq.Init.Datatypes <> nil constr
prf 11923:11930 <> derive_Q
R11994:12003 type_derivation <> derivation ind
R12017:12021 type_derivation <> funty def
R12079:12083 type_derivation <> funty def
R12139:12143 type_derivation <> funty def
R12149:12151 operator_types <> ty2 var
R12145:12147 operator_types <> ty1 var
R12086:12090 type_derivation <> funty def
R12097:12101 type_derivation <> funty def
R12107:12109 operator_types <> ty2 var
R12103:12105 operator_types <> ty2 var
R12092:12094 operator_types <> ty2 var
R12024:12026 LamSF_Terms <> Abs constr
R12029:12033 type_derivation <> funty def
R12046:12049 LamSF_Terms <> lift def
R12053:12055 operator_types <> ty2 var
R12036:12040 type_derivation <> varty def
R12011:12014 Components <> q_op def
R12005:12009 operator_types <> gamma var
R11981:11983 type_derivation <> wfs ind
R11985:11987 operator_types <> ty2 var
R11970:11972 type_derivation <> wfs ind
R11974:11976 operator_types <> ty1 var
R11957:11959 type_derivation <> wfc ind
R11961:11965 operator_types <> gamma var
R12181:12195 type_derivation <> derive_instance thm
R12206:12214 type_derivation <> derive_op constr
R12225:12234 operator_types <> instance_Q thm
prf 12249:12259 <> instance_Q2
R12310:12316 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R12336:12337 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R12380:12384 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R12340:12342 Coq.Init.Logic <> :type_scope:x_'='_x not
R12338:12339 operator_types <> ty var
R12343:12347 type_derivation <> funty def
R12354:12358 type_derivation <> funty def
R12365:12369 type_derivation <> funty def
R12375:12377 operator_types <> ty5 var
R12371:12373 operator_types <> ty3 var
R12360:12362 operator_types <> ty2 var
R12349:12351 operator_types <> ty1 var
R12401:12404 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R12385:12392 type_derivation <> instance def
R12398:12400 operator_types <> ty5 var
R12394:12396 operator_types <> ty4 var
R12445:12449 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R12405:12412 type_derivation <> instance def
R12419:12423 type_derivation <> funty def
R12430:12434 type_derivation <> funty def
R12440:12442 operator_types <> ty4 var
R12436:12438 operator_types <> ty4 var
R12425:12427 operator_types <> ty4 var
R12414:12416 operator_types <> ty2 var
R12450:12457 type_derivation <> instance def
R12464:12466 LamSF_Terms <> Abs constr
R12469:12473 type_derivation <> funty def
R12486:12489 LamSF_Terms <> lift def
R12493:12495 operator_types <> ty4 var
R12476:12480 type_derivation <> varty def
R12459:12461 operator_types <> ty1 var
R12300:12301 type_derivation <> wf ind
R12303:12304 operator_types <> ty var
R12275:12282 type_derivation <> instance def
R12294:12295 operator_types <> ty var
R12284:12287 type_derivation <> opty def
R12289:12291 LamSF_Terms <> Qop constr
R12517:12520 type_derivation <> opty def
R12523:12527 type_derivation <> quant def
prf 12668:12677 <> instance_U
R12706:12713 type_derivation <> instance def
R12745:12749 type_derivation <> funty def
R12961:12965 type_derivation <> funty def
R12971:12973 operator_types <> ty1 var