-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathtype_derivation_resi.glob
446 lines (446 loc) · 19.3 KB
/
type_derivation_resi.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
DIGEST d452a6dae5ac5ac1c47778e94d60dce8
Ftype_derivation_resi
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
ind 2425:2439 <> derivation_resi
constr 2483:2489 <> resi_op
constr 2621:2628 <> resi_var
constr 2786:2794 <> resi_weak
constr 2953:2960 <> resi_abs
constr 3115:3122 <> resi_app
constr 3344:3352 <> resi_gen1
constr 3488:3497 <> resi_push1
R2463:2467 LamSF_Terms <> lamSF ind
R2454:2458 LamSF_Terms <> lamSF ind
R2443:2449 type_derivation <> context def
R2586:2600 type_derivation_resi <> derivation_resi ind
R2615:2616 type_derivation_resi <> ty var
R2609:2610 LamSF_Terms <> Op constr
R2612:2612 type_derivation_resi <> o var
R2602:2606 type_derivation_resi <> gamma var
R2537:2539 type_derivation <> wfc ind
R2541:2545 type_derivation_resi <> gamma var
R2513:2520 type_derivation <> instance def
R2531:2532 type_derivation_resi <> ty var
R2523:2526 type_derivation <> opty def
R2528:2528 type_derivation_resi <> o var
R2739:2753 type_derivation_resi <> derivation_resi ind
R2780:2782 type_derivation_resi <> ty2 var
R2773:2775 LamSF_Terms <> Ref constr
R2756:2759 Coq.Init.Datatypes <> cons constr
R2765:2769 type_derivation_resi <> gamma var
R2761:2763 type_derivation_resi <> ty1 var
R2688:2690 type_derivation <> wfs ind
R2692:2694 type_derivation_resi <> ty1 var
R2675:2677 type_derivation <> wfc ind
R2679:2683 type_derivation_resi <> gamma var
R2655:2662 type_derivation <> instance def
R2668:2670 type_derivation_resi <> ty2 var
R2664:2666 type_derivation_resi <> ty1 var
R2903:2917 type_derivation_resi <> derivation_resi ind
R2948:2949 type_derivation_resi <> ty var
R2937:2939 LamSF_Terms <> Ref constr
R2942:2942 Coq.Init.Datatypes <> S constr
R2944:2944 type_derivation_resi <> i var
R2920:2923 Coq.Init.Datatypes <> cons constr
R2929:2933 type_derivation_resi <> gamma var
R2925:2927 type_derivation_resi <> ty1 var
R2858:2860 type_derivation <> wfs ind
R2862:2864 type_derivation_resi <> ty1 var
R2822:2836 type_derivation_resi <> derivation_resi ind
R2852:2853 type_derivation_resi <> ty var
R2845:2847 LamSF_Terms <> Ref constr
R2849:2849 type_derivation_resi <> i var
R2838:2842 type_derivation_resi <> gamma var
R3067:3081 type_derivation_resi <> derivation_resi ind
R3098:3102 type_derivation <> funty def
R3108:3110 type_derivation_resi <> ty2 var
R3104:3106 type_derivation_resi <> ty1 var
R3090:3092 LamSF_Terms <> Abs constr
R3094:3094 type_derivation_resi <> t var
R3083:3087 type_derivation_resi <> gamma var
R3008:3022 type_derivation_resi <> derivation_resi ind
R3043:3045 type_derivation_resi <> ty2 var
R3041:3041 type_derivation_resi <> t var
R3025:3028 Coq.Init.Datatypes <> cons constr
R3034:3038 type_derivation_resi <> gamma var
R3030:3032 type_derivation_resi <> ty1 var
R3306:3320 type_derivation_resi <> derivation_resi ind
R3338:3340 type_derivation_resi <> ty2 var
R3329:3331 LamSF_Terms <> App constr
R3335:3335 type_derivation_resi <> u var
R3333:3333 type_derivation_resi <> t var
R3322:3326 type_derivation_resi <> gamma var
R3229:3238 type_derivation <> derivation ind
R3248:3250 type_derivation_resi <> ty1 var
R3246:3246 type_derivation_resi <> u var
R3240:3244 type_derivation_resi <> gamma var
R3169:3183 type_derivation_resi <> derivation_resi ind
R3194:3198 type_derivation <> funty def
R3204:3206 type_derivation_resi <> ty2 var
R3200:3202 type_derivation_resi <> ty1 var
R3191:3191 type_derivation_resi <> t var
R3185:3189 type_derivation_resi <> gamma var
R3453:3467 type_derivation_resi <> derivation_resi ind
R3478:3480 LamSF_Terms <> Abs constr
R3482:3483 type_derivation_resi <> ty var
R3475:3475 type_derivation_resi <> t var
R3469:3473 type_derivation_resi <> gamma var
R3374:3388 type_derivation_resi <> derivation_resi ind
R3413:3414 type_derivation_resi <> ty var
R3411:3411 type_derivation_resi <> t var
R3391:3393 Coq.Lists.List <> map def
R3404:3408 type_derivation_resi <> gamma var
R3396:3399 LamSF_Terms <> lift def
R3594:3608 type_derivation_resi <> derivation_resi ind
R3618:3620 type_derivation_resi <> ty2 var
R3616:3616 type_derivation_resi <> t var
R3610:3614 type_derivation_resi <> gamma var
R3578:3582 type_derivation <> push1 ind
R3587:3589 type_derivation_resi <> ty2 var
R3584:3585 type_derivation_resi <> ty var
R3520:3534 type_derivation_resi <> derivation_resi ind
R3544:3545 type_derivation_resi <> ty var
R3542:3542 type_derivation_resi <> t var
R3536:3540 type_derivation_resi <> gamma var
R3641:3647 type_derivation_resi <> resi_op constr
R3649:3656 type_derivation_resi <> resi_var constr
R3658:3666 type_derivation_resi <> resi_weak constr
R3668:3675 type_derivation_resi <> resi_abs constr
R3677:3684 type_derivation_resi <> resi_app constr
R3686:3694 type_derivation_resi <> resi_gen1 constr
R3696:3705 type_derivation_resi <> resi_push1 constr
prf 3717:3742 <> lift_rec_ty_preserves_resi
R3809:3823 type_derivation_resi <> derivation_resi ind
R3870:3877 LamSF_Terms <> lift_rec def
R3884:3884 type_derivation_resi <> k var
R3882:3882 type_derivation_resi <> n var
R3879:3880 type_derivation_resi <> ty var
R3867:3867 type_derivation_resi <> t var
R3826:3828 Coq.Lists.List <> map def
R3860:3864 type_derivation_resi <> gamma var
R3842:3849 LamSF_Terms <> lift_rec def
R3857:3857 type_derivation_resi <> k var
R3855:3855 type_derivation_resi <> n var
R3851:3853 type_derivation_resi <> ty0 var
R3765:3779 type_derivation_resi <> derivation_resi ind
R3789:3790 type_derivation_resi <> ty var
R3787:3787 type_derivation_resi <> t var
R3781:3785 type_derivation_resi <> gamma var
R3959:3965 type_derivation_resi <> resi_op constr
R3978:3981 type_derivation <> opty def
R3992:3999 LamSF_Terms <> lift_rec def
R4002:4005 type_derivation <> opty def
R3992:3999 LamSF_Terms <> lift_rec def
R4002:4005 type_derivation <> opty def
R3978:3981 type_derivation <> opty def
R4054:4080 type_derivation <> lift_rec_preserves_instance thm
R4101:4108 type_derivation_resi <> resi_var constr
R4120:4146 type_derivation <> lift_rec_preserves_instance thm
R4167:4174 type_derivation_resi <> resi_abs constr
R4221:4228 LamSF_Terms <> lift_rec def
R4206:4213 type_derivation_resi <> resi_app constr
R4221:4228 LamSF_Terms <> lift_rec def
R4206:4213 type_derivation_resi <> resi_app constr
R4256:4260 type_derivation <> funty def
R4282:4289 LamSF_Terms <> lift_rec def
R4263:4270 LamSF_Terms <> lift_rec def
R4308:4315 LamSF_Terms <> lift_rec def
R4318:4322 type_derivation <> funty def
R4308:4315 LamSF_Terms <> lift_rec def
R4318:4322 type_derivation <> funty def
R4256:4260 type_derivation <> funty def
R4282:4289 LamSF_Terms <> lift_rec def
R4263:4270 LamSF_Terms <> lift_rec def
R4369:4396 type_derivation <> lift_rec_ty_preserves_derive thm
R4418:4426 type_derivation_resi <> resi_gen1 constr
R4438:4440 Coq.Lists.List <> map def
R4452:4454 Coq.Lists.List <> map def
R4467:4471 LamSF_Terms <> lamSF ind
R4476:4483 LamSF_Terms <> lift_rec def
R4485:4487 type_derivation_resi <> ty0 var
R4443:4446 LamSF_Terms <> lift def
R4509:4511 Coq.Lists.List <> map def
R4556:4558 Coq.Lists.List <> map def
R4561:4564 LamSF_Terms <> lift def
R4524:4528 LamSF_Terms <> lamSF ind
R4533:4540 LamSF_Terms <> lift_rec def
R4547:4547 Coq.Init.Datatypes <> S constr
R4542:4544 type_derivation_resi <> ty0 var
R4509:4511 Coq.Lists.List <> map def
R4556:4558 Coq.Lists.List <> map def
R4561:4564 LamSF_Terms <> lift def
R4524:4528 LamSF_Terms <> lamSF ind
R4533:4540 LamSF_Terms <> lift_rec def
R4547:4547 Coq.Init.Datatypes <> S constr
R4542:4544 type_derivation_resi <> ty0 var
R4438:4440 Coq.Lists.List <> map def
R4452:4454 Coq.Lists.List <> map def
R4467:4471 LamSF_Terms <> lamSF ind
R4476:4483 LamSF_Terms <> lift_rec def
R4485:4487 type_derivation_resi <> ty0 var
R4443:4446 LamSF_Terms <> lift def
R4660:4663 LamSF_Terms <> lift def
R4674:4686 LamSF_Substitution_term <> lift_lift_rec thm
R4674:4686 LamSF_Substitution_term <> lift_lift_rec thm
R4724:4733 type_derivation_resi <> resi_push1 constr
R4744:4767 type_derivation <> lift_rec_preserves_push1 thm
prf 4785:4818 <> subst_rec_ty_preserves_derive_resi
R4899:4913 type_derivation_resi <> derivation_resi ind
R4975:4983 LamSF_Terms <> subst_rec def
R4992:4992 type_derivation_resi <> k var
R4988:4990 type_derivation_resi <> ty1 var
R4985:4986 type_derivation_resi <> ty var
R4960:4960 type_derivation_resi <> t var
R4916:4918 Coq.Lists.List <> map def
R4953:4957 type_derivation_resi <> gamma var
R4932:4940 LamSF_Terms <> subst_rec def
R4950:4950 type_derivation_resi <> k var
R4946:4948 type_derivation_resi <> ty1 var
R4942:4944 type_derivation_resi <> ty0 var
R4887:4889 type_derivation <> wfs ind
R4891:4893 type_derivation_resi <> ty1 var
R4842:4856 type_derivation_resi <> derivation_resi ind
R4866:4867 type_derivation_resi <> ty var
R4864:4864 type_derivation_resi <> t var
R4858:4862 type_derivation_resi <> gamma var
R5068:5074 type_derivation_resi <> resi_op constr
R5086:5089 type_derivation <> opty def
R5100:5108 LamSF_Terms <> subst_rec def
R5111:5114 type_derivation <> opty def
R5100:5108 LamSF_Terms <> subst_rec def
R5111:5114 type_derivation <> opty def
R5086:5089 type_derivation <> opty def
R5159:5186 type_derivation <> subst_rec_preserves_instance thm
R5207:5214 type_derivation_resi <> resi_var constr
R5225:5252 type_derivation <> subst_rec_preserves_instance thm
R5264:5286 type_derivation <> subst_rec_preserves_wfs thm
R5307:5315 type_derivation_resi <> resi_weak constr
R5326:5348 type_derivation <> subst_rec_preserves_wfs thm
R5369:5376 type_derivation_resi <> resi_abs constr
R5410:5417 type_derivation_resi <> resi_app constr
R5431:5459 type_derivation <> subst_rec_ty_preserves_derive thm
R5431:5459 type_derivation <> subst_rec_ty_preserves_derive thm
R5518:5536 type_derivation <> derive_implies_wfcs thm
R5556:5570 type_derivation_resi <> derivation_resi ind
R5667:5675 LamSF_Terms <> subst_rec def
R5685:5685 Coq.Init.Datatypes <> S constr
R5583:5585 Coq.Lists.List <> map def
R5633:5635 Coq.Lists.List <> map def
R5638:5641 LamSF_Terms <> lift def
R5598:5602 LamSF_Terms <> lamSF ind
R5607:5615 LamSF_Terms <> subst_rec def
R5626:5626 Coq.Init.Datatypes <> S constr
R5617:5619 type_derivation_resi <> ty0 var
R5556:5570 type_derivation_resi <> derivation_resi ind
R5667:5675 LamSF_Terms <> subst_rec def
R5685:5685 Coq.Init.Datatypes <> S constr
R5583:5585 Coq.Lists.List <> map def
R5633:5635 Coq.Lists.List <> map def
R5638:5641 LamSF_Terms <> lift def
R5598:5602 LamSF_Terms <> lamSF ind
R5607:5615 LamSF_Terms <> subst_rec def
R5626:5626 Coq.Init.Datatypes <> S constr
R5617:5619 type_derivation_resi <> ty0 var
R5718:5720 Coq.Lists.List <> map def
R5768:5770 Coq.Lists.List <> map def
R5773:5776 LamSF_Terms <> lift def
R5733:5737 LamSF_Terms <> lamSF ind
R5742:5750 LamSF_Terms <> subst_rec def
R5761:5761 Coq.Init.Datatypes <> S constr
R5752:5754 type_derivation_resi <> ty0 var
R5795:5797 Coq.Lists.List <> map def
R5809:5811 Coq.Lists.List <> map def
R5824:5828 LamSF_Terms <> lamSF ind
R5833:5841 LamSF_Terms <> subst_rec def
R5843:5845 type_derivation_resi <> ty0 var
R5800:5803 LamSF_Terms <> lift def
R5795:5797 Coq.Lists.List <> map def
R5809:5811 Coq.Lists.List <> map def
R5824:5828 LamSF_Terms <> lamSF ind
R5833:5841 LamSF_Terms <> subst_rec def
R5843:5845 type_derivation_resi <> ty0 var
R5800:5803 LamSF_Terms <> lift def
R5718:5720 Coq.Lists.List <> map def
R5768:5770 Coq.Lists.List <> map def
R5773:5776 LamSF_Terms <> lift def
R5733:5737 LamSF_Terms <> lamSF ind
R5742:5750 LamSF_Terms <> subst_rec def
R5761:5761 Coq.Init.Datatypes <> S constr
R5752:5754 type_derivation_resi <> ty0 var
R5936:5939 LamSF_Terms <> lift def
R5950:5968 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R5950:5968 LamSF_Substitution_term <> subst_rec_lift_rec1 thm
R6001:6010 type_derivation_resi <> resi_push1 constr
R6021:6045 type_derivation <> subst_rec_preserves_push1 thm
def 6068:6081 <> preserves_resi
R6089:6095 LamSF_Tactics <> termred def
R6181:6195 type_derivation_resi <> derivation_resi ind
R6205:6207 type_derivation_resi <> ty2 var
R6203:6203 type_derivation_resi <> t var
R6197:6201 type_derivation_resi <> gamma var
R6150:6164 type_derivation_resi <> derivation_resi ind
R6174:6176 type_derivation_resi <> ty1 var
R6172:6172 type_derivation_resi <> t var
R6166:6170 type_derivation_resi <> gamma var
R6118:6120 type_derivation_resi <> red var
R6126:6128 type_derivation_resi <> ty2 var
R6122:6124 type_derivation_resi <> ty1 var
prf 6218:6242 <> preserves_resi_multi_step
R6280:6293 type_derivation_resi <> preserves_resi def
R6296:6305 LamSF_Tactics <> multi_step ind
R6307:6309 type_derivation_resi <> red var
R6258:6271 type_derivation_resi <> preserves_resi def
R6273:6275 type_derivation_resi <> red var
prf 6398:6416 <> preserves_resi_push
R6420:6433 type_derivation_resi <> preserves_resi def
R6435:6438 type_derivation <> push def
R6457:6481 type_derivation_resi <> preserves_resi_multi_step thm
R6508:6517 type_derivation_resi <> resi_push1 constr
prf 6534:6567 <> derivation_resi_implies_derivation
R6621:6630 type_derivation <> derivation ind
R6640:6641 type_derivation_resi <> ty var
R6638:6638 type_derivation_resi <> t var
R6632:6636 type_derivation_resi <> gamma var
R6591:6605 type_derivation_resi <> derivation_resi ind
R6615:6616 type_derivation_resi <> ty var
R6613:6613 type_derivation_resi <> t var
R6607:6611 type_derivation_resi <> gamma var
R6721:6735 type_derivation <> derive_instance thm
R6755:6769 type_derivation <> derive_instance thm
R6755:6769 type_derivation <> derive_instance thm
R6781:6790 type_derivation <> derive_var constr
prf 6814:6841 <> derive_resi_instance_context
R6947:6961 type_derivation_resi <> derivation_resi ind
R6972:6973 type_derivation_resi <> ty var
R6970:6970 type_derivation_resi <> t var
R6963:6968 type_derivation_resi <> gamma2 var
R6913:6928 type_derivation <> instance_context ind
R6937:6942 type_derivation_resi <> gamma1 var
R6930:6935 type_derivation_resi <> gamma2 var
R6866:6880 type_derivation_resi <> derivation_resi ind
R6891:6892 type_derivation_resi <> ty var
R6889:6889 type_derivation_resi <> t var
R6882:6887 type_derivation_resi <> gamma1 var
R7075:7081 type_derivation_resi <> resi_op constr
R7092:7120 type_derivation <> instance_context_reflects_wfc thm
R7164:7171 type_derivation_resi <> resi_var constr
R7182:7195 LamSF_Tactics <> transitive_red thm
R7207:7235 type_derivation <> instance_context_reflects_wfc thm
R7246:7265 type_derivation <> instance_implies_wfs thm
R7320:7328 type_derivation_resi <> resi_weak constr
R7339:7358 type_derivation <> instance_implies_wfs thm
R7379:7386 type_derivation_resi <> resi_abs constr
R7410:7430 type_derivation <> instance_context_cons constr
R7441:7448 LamSF_Tactics <> zero_red constr
R7469:7476 type_derivation_resi <> resi_app constr
R7487:7509 type_derivation <> derive_instance_context thm
R7530:7538 type_derivation_resi <> resi_gen1 constr
R7562:7596 type_derivation <> lift_rec_preserves_instance_context thm
R7617:7626 type_derivation_resi <> resi_push1 constr
prf 7644:7653 <> resi_inst1
R7743:7757 type_derivation_resi <> derivation_resi ind
R7767:7769 type_derivation_resi <> ty2 var
R7765:7765 type_derivation_resi <> t var
R7759:7763 type_derivation_resi <> gamma var
R7722:7730 type_derivation <> instance1 ind
R7736:7738 type_derivation_resi <> ty2 var
R7732:7734 type_derivation_resi <> ty1 var
R7678:7692 type_derivation_resi <> derivation_resi ind
R7702:7704 type_derivation_resi <> ty1 var
R7700:7700 type_derivation_resi <> t var
R7694:7698 type_derivation_resi <> gamma var
R7860:7866 type_derivation_resi <> resi_op constr
R7876:7889 LamSF_Tactics <> transitive_red thm
R7876:7889 LamSF_Tactics <> transitive_red thm
R7929:7936 type_derivation_resi <> resi_var constr
R7946:7959 LamSF_Tactics <> transitive_red thm
R7946:7959 LamSF_Tactics <> transitive_red thm
R8019:8026 type_derivation_resi <> resi_abs constr
R8019:8026 type_derivation_resi <> resi_abs constr
R8038:8065 type_derivation_resi <> derive_resi_instance_context thm
R8076:8096 type_derivation <> instance_context_cons constr
R8158:8178 type_derivation <> instance_context_cons constr
R8189:8196 LamSF_Tactics <> zero_red constr
R8217:8224 type_derivation_resi <> resi_app constr
R8248:8261 type_derivation <> instance_funty constr
R8272:8290 type_derivation <> derive_implies_wfcs thm
R8340:8354 type_derivation_resi <> derivation_resi ind
R8415:8423 LamSF_Terms <> subst_rec def
R8357:8359 Coq.Lists.List <> map def
R8391:8393 Coq.Lists.List <> map def
R8396:8399 LamSF_Terms <> lift def
R8371:8379 LamSF_Terms <> subst_rec def
R8381:8381 type_derivation_resi <> M var
R8340:8354 type_derivation_resi <> derivation_resi ind
R8415:8423 LamSF_Terms <> subst_rec def
R8357:8359 Coq.Lists.List <> map def
R8391:8393 Coq.Lists.List <> map def
R8396:8399 LamSF_Terms <> lift def
R8371:8379 LamSF_Terms <> subst_rec def
R8381:8381 type_derivation_resi <> M var
R8447:8480 type_derivation_resi <> subst_rec_ty_preserves_derive_resi thm
R8552:8554 Coq.Init.Logic <> :type_scope:x_'='_x not
R8491:8493 Coq.Lists.List <> map def
R8533:8535 Coq.Lists.List <> map def
R8538:8541 LamSF_Terms <> lift def
R8504:8508 LamSF_Terms <> lamSF ind
R8513:8521 LamSF_Terms <> subst_rec def
R8523:8523 type_derivation_resi <> M var
R8552:8554 Coq.Init.Logic <> :type_scope:x_'='_x not
R8491:8493 Coq.Lists.List <> map def
R8533:8535 Coq.Lists.List <> map def
R8538:8541 LamSF_Terms <> lift def
R8504:8508 LamSF_Terms <> lamSF ind
R8513:8521 LamSF_Terms <> subst_rec def
R8523:8523 type_derivation_resi <> M var
R8624:8627 LamSF_Terms <> lift def
R8638:8655 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8638:8655 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8677:8689 LamSF_Substitution_term <> lift_rec_null thm
R8677:8689 LamSF_Substitution_term <> lift_rec_null thm
R8741:8749 type_derivation_resi <> resi_gen1 constr
R8769:8775 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8779:8780 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8797:8800 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8781:8789 type_derivation <> instance1 ind
R8794:8796 type_derivation_resi <> ty5 var
R8801:8804 type_derivation <> push def
R8806:8808 type_derivation_resi <> ty5 var
R8769:8775 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8779:8780 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R8797:8800 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R8781:8789 type_derivation <> instance1 ind
R8794:8796 type_derivation_resi <> ty5 var
R8801:8804 type_derivation <> push def
R8806:8808 type_derivation_resi <> ty5 var
R8826:8840 type_derivation <> push1_instance1 thm
R8863:8877 type_derivation_resi <> derivation_resi ind
R8863:8877 type_derivation_resi <> derivation_resi ind
R8915:8933 type_derivation_resi <> preserves_resi_push thm
prf 8951:8984 <> derivation_implies_derivation_resi
R9033:9047 type_derivation_resi <> derivation_resi ind
R9057:9058 type_derivation_resi <> ty var
R9055:9055 type_derivation_resi <> t var
R9049:9053 type_derivation_resi <> gamma var
R9007:9016 type_derivation <> derivation ind
R9026:9027 type_derivation_resi <> ty var
R9024:9024 type_derivation_resi <> t var
R9018:9022 type_derivation_resi <> gamma var
R9137:9143 type_derivation_resi <> resi_op constr
R9154:9161 LamSF_Tactics <> zero_red constr
R9183:9190 type_derivation_resi <> resi_var constr
R9201:9208 LamSF_Tactics <> zero_red constr
R9228:9237 type_derivation_resi <> resi_inst1 thm