forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Eta.glob
633 lines (633 loc) · 19.6 KB
/
Eta.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
DIGEST 510d1bcd5ef0802cd5d04a8be682bbc5
FEta
R1992:1996 Coq.Arith.Arith <> <> lib
R2014:2016 Coq.Arith.Max <> <> lib
R2035:2038 Test <> <> lib
R2056:2062 General <> <> lib
R2081:2091 LamSF_Terms <> <> lib
R2109:2131 LamSF_Substitution_term <> <> lib
R2149:2161 LamSF_Tactics <> <> lib
R2179:2192 Beta_Reduction <> <> lib
R2210:2225 LamSF_Confluence <> <> lib
R2243:2254 SF_reduction <> <> lib
R2272:2286 LamSF_reduction <> <> lib
R2304:2315 LamSF_Normal <> <> lib
R2333:2344 LamSF_Closed <> <> lib
R2362:2371 LamSF_Eval <> <> lib
R2389:2393 Equal <> <> lib
ind 2409:2419 <> beta_eta_eq
constr 2438:2447 <> ref_etared
constr 2493:2501 <> op_etared
constr 2545:2554 <> app_etared
constr 2691:2700 <> abs_etared
constr 2771:2778 <> beta_red
constr 2922:2928 <> eta_red
constr 3058:3065 <> s_etared
constr 3319:3326 <> k_etared
constr 3439:3449 <> symm_etared
constr 3507:3518 <> trans_etared
R2423:2429 LamSF_Tactics <> termred def
R2461:2471 Eta <> beta_eta_eq ind
R2482:2484 LamSF_Terms <> Ref constr
R2486:2486 Eta <> i var
R2474:2476 LamSF_Terms <> Ref constr
R2478:2478 Eta <> i var
R2515:2525 Eta <> beta_eta_eq ind
R2535:2536 LamSF_Terms <> Op constr
R2538:2538 Eta <> o var
R2528:2529 LamSF_Terms <> Op constr
R2531:2531 Eta <> o var
R2600:2609 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2624:2628 LamSF_Terms <> lamSF ind
R2647:2650 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2651:2661 Eta <> beta_eta_eq ind
R2674:2676 LamSF_Terms <> App constr
R2681:2682 Eta <> N' var
R2678:2679 Eta <> M' var
R2664:2666 LamSF_Terms <> App constr
R2670:2670 Eta <> N var
R2668:2668 Eta <> M var
R2631:2641 Eta <> beta_eta_eq ind
R2645:2646 Eta <> N' var
R2643:2643 Eta <> N var
R2584:2594 Eta <> beta_eta_eq ind
R2598:2599 Eta <> M' var
R2596:2596 Eta <> M var
R2734:2737 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2738:2748 Eta <> beta_eta_eq ind
R2759:2761 LamSF_Terms <> Abs constr
R2763:2764 Eta <> M' var
R2751:2753 LamSF_Terms <> Abs constr
R2755:2755 Eta <> M var
R2718:2728 Eta <> beta_eta_eq ind
R2732:2733 Eta <> M' var
R2730:2730 Eta <> M var
R2800:2804 LamSF_Terms <> lamSF ind
R2837:2840 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2857:2875 Coq.Init.Logic <> :type_scope:x_'->'_x not
R2876:2886 Eta <> beta_eta_eq ind
R2905:2909 LamSF_Terms <> subst def
R2914:2915 Eta <> M' var
R2911:2912 Eta <> N' var
R2889:2891 LamSF_Terms <> App constr
R2901:2901 Eta <> N var
R2894:2896 LamSF_Terms <> Abs constr
R2898:2898 Eta <> M var
R2841:2851 Eta <> beta_eta_eq ind
R2855:2856 Eta <> N' var
R2853:2853 Eta <> N var
R2821:2831 Eta <> beta_eta_eq ind
R2835:2836 Eta <> M' var
R2833:2833 Eta <> M var
R2946:2950 LamSF_Terms <> lamSF ind
R2983:3000 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3001:3011 Eta <> beta_eta_eq ind
R3050:3051 Eta <> M' var
R3014:3016 LamSF_Terms <> Abs constr
R3019:3021 LamSF_Terms <> App constr
R3041:3043 LamSF_Terms <> Ref constr
R3024:3031 LamSF_Terms <> lift_rec def
R3033:3033 Eta <> M var
R2967:2977 Eta <> beta_eta_eq ind
R2981:2982 Eta <> M' var
R2979:2979 Eta <> M var
R3093:3097 LamSF_Terms <> lamSF ind
R3130:3133 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3150:3153 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3170:3204 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3205:3215 Eta <> beta_eta_eq ind
R3286:3288 LamSF_Terms <> App constr
R3303:3305 LamSF_Terms <> App constr
R3310:3311 Eta <> P' var
R3307:3308 Eta <> N' var
R3291:3293 LamSF_Terms <> App constr
R3298:3299 Eta <> P' var
R3295:3296 Eta <> M' var
R3238:3240 LamSF_Terms <> App constr
R3263:3263 Eta <> P var
R3243:3245 LamSF_Terms <> App constr
R3260:3260 Eta <> N var
R3248:3250 LamSF_Terms <> App constr
R3257:3257 Eta <> M var
R3252:3255 SF_reduction <> s_op def
R3154:3164 Eta <> beta_eta_eq ind
R3168:3169 Eta <> P' var
R3166:3166 Eta <> P var
R3134:3144 Eta <> beta_eta_eq ind
R3148:3149 Eta <> N' var
R3146:3146 Eta <> N var
R3114:3124 Eta <> beta_eta_eq ind
R3128:3129 Eta <> M' var
R3126:3126 Eta <> M var
R3365:3384 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3385:3395 Eta <> beta_eta_eq ind
R3431:3432 Eta <> M' var
R3398:3400 LamSF_Terms <> App constr
R3428:3428 Eta <> N var
R3403:3405 LamSF_Terms <> App constr
R3425:3425 Eta <> M var
R3408:3410 LamSF_Terms <> App constr
R3418:3419 LamSF_Terms <> Op constr
R3421:3421 Eta <> o var
R3412:3415 SF_reduction <> f_op def
R3349:3359 Eta <> beta_eta_eq ind
R3363:3364 Eta <> M' var
R3361:3361 Eta <> M var
R3482:3485 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3486:3496 Eta <> beta_eta_eq ind
R3501:3501 Eta <> M var
R3498:3499 Eta <> M' var
R3466:3476 Eta <> beta_eta_eq ind
R3480:3481 Eta <> M' var
R3478:3478 Eta <> M var
R3551:3554 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3570:3573 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3574:3584 Eta <> beta_eta_eq ind
R3588:3588 Eta <> P var
R3586:3586 Eta <> M var
R3555:3565 Eta <> beta_eta_eq ind
R3569:3569 Eta <> P var
R3567:3567 Eta <> N var
R3536:3546 Eta <> beta_eta_eq ind
R3550:3550 Eta <> N var
R3548:3548 Eta <> M var
prf 3723:3744 <> reflective_beta_eta_eq
R3748:3757 LamSF_Tactics <> reflective def
R3759:3769 Eta <> beta_eta_eq ind
prf 3859:3883 <> preserves_abs_beta_eta_eq
R3887:3899 LamSF_Tactics <> preserves_abs def
R3901:3911 Eta <> beta_eta_eq ind
prf 3993:4017 <> preserves_app_beta_eta_eq
R4021:4033 LamSF_Tactics <> preserves_app def
R4035:4045 Eta <> beta_eta_eq ind
def 4133:4138 <> stable
R4145:4151 LamSF_Tactics <> termred def
R4176:4179 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4181:4183 Coq.Init.Logic <> :type_scope:x_'='_x not
R4180:4180 Eta <> N var
R4184:4184 Eta <> M var
R4169:4171 Eta <> red var
R4175:4175 Eta <> N var
R4173:4173 Eta <> M var
prf 4194:4210 <> stable_multi_step
R4240:4243 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4244:4249 Eta <> stable def
R4268:4268 Eta <> M var
R4252:4261 LamSF_Tactics <> multi_step ind
R4263:4265 Eta <> red var
R4228:4233 Eta <> stable def
R4239:4239 Eta <> M var
R4235:4237 Eta <> red var
R4328:4329 Coq.Init.Logic <> :type_scope:x_'='_x not
R4328:4329 Coq.Init.Logic <> :type_scope:x_'='_x not
prf 4392:4401 <> stable_seq
R4438:4441 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4455:4458 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4459:4464 Eta <> stable def
R4489:4489 Eta <> M var
R4467:4476 LamSF_Tactics <> sequential ind
R4483:4486 Eta <> red2 var
R4478:4481 Eta <> red1 var
R4442:4447 Eta <> stable def
R4454:4454 Eta <> M var
R4449:4452 Eta <> red2 var
R4425:4430 Eta <> stable def
R4437:4437 Eta <> M var
R4432:4435 Eta <> red1 var
R4538:4540 Coq.Init.Logic <> :type_scope:x_'='_x not
R4538:4540 Coq.Init.Logic <> :type_scope:x_'='_x not
def 4587:4589 <> ref
R4594:4596 LamSF_Terms <> Ref constr
def 4611:4612 <> ap
R4617:4619 LamSF_Terms <> App constr
def 4635:4637 <> abs
R4642:4644 LamSF_Terms <> Abs constr
def 4659:4663 <> abs_S
R4669:4671 Eta <> abs def
R4674:4676 Eta <> abs def
R4679:4681 Eta <> abs def
R4684:4685 Eta <> ap def
R4709:4710 Eta <> ap def
R4721:4723 Eta <> ref def
R4713:4715 Eta <> ref def
R4688:4689 Eta <> ap def
R4700:4702 Eta <> ref def
R4692:4694 Eta <> ref def
def 4747:4751 <> abs_K
R4757:4759 Eta <> abs def
R4762:4764 Eta <> abs def
R4767:4769 Eta <> ref def
def 4788:4792 <> abs_I
R4798:4800 Eta <> abs def
R4803:4805 Eta <> ref def
def 4823:4828 <> abs_KI
R4834:4836 Eta <> abs def
R4839:4841 Eta <> abs def
R4844:4846 Eta <> ref def
prf 4862:4865 <> eq_I
R4869:4879 Eta <> beta_eta_eq ind
R4886:4890 Eta <> abs_I def
R4881:4884 SF_reduction <> i_op def
R4920:4930 Eta <> beta_eta_eq ind
R4957:4960 SF_reduction <> i_op def
R4934:4936 Eta <> abs def
R4939:4940 Eta <> ap def
R4948:4950 Eta <> ref def
R4942:4945 SF_reduction <> i_op def
R4920:4930 Eta <> beta_eta_eq ind
R4957:4960 SF_reduction <> i_op def
R4934:4936 Eta <> abs def
R4939:4940 Eta <> ap def
R4948:4950 Eta <> ref def
R4942:4945 SF_reduction <> i_op def
R4972:4974 Eta <> abs def
R4977:4978 Eta <> ap def
R5013:5015 Coq.Init.Logic <> :type_scope:x_'='_x not
R4996:5003 LamSF_Terms <> lift_rec def
R5005:5008 SF_reduction <> i_op def
R5016:5019 SF_reduction <> i_op def
R5013:5015 Coq.Init.Logic <> :type_scope:x_'='_x not
R4996:5003 LamSF_Terms <> lift_rec def
R5005:5008 SF_reduction <> i_op def
R5016:5019 SF_reduction <> i_op def
R5075:5081 Eta <> eta_red constr
R5091:5101 Eta <> beta_eta_eq ind
R5127:5131 Eta <> abs_I def
R5104:5106 Eta <> abs def
R5109:5110 Eta <> ap def
R5118:5120 Eta <> ref def
R5112:5115 SF_reduction <> i_op def
R5091:5101 Eta <> beta_eta_eq ind
R5127:5131 Eta <> abs_I def
R5104:5106 Eta <> abs def
R5109:5110 Eta <> ap def
R5118:5120 Eta <> ref def
R5112:5115 SF_reduction <> i_op def
R5142:5146 Eta <> abs_I def
R5166:5190 Eta <> preserves_abs_beta_eta_eq thm
R5166:5190 Eta <> preserves_abs_beta_eta_eq thm
R5213:5214 Eta <> ap def
R5244:5246 LamSF_Terms <> App constr
R5267:5269 LamSF_Terms <> App constr
R5277:5279 Eta <> ref def
R5271:5274 SF_reduction <> k_op def
R5249:5251 LamSF_Terms <> App constr
R5259:5261 Eta <> ref def
R5253:5256 SF_reduction <> k_op def
R5225:5236 Eta <> trans_etared constr
R5244:5246 LamSF_Terms <> App constr
R5267:5269 LamSF_Terms <> App constr
R5277:5279 Eta <> ref def
R5271:5274 SF_reduction <> k_op def
R5249:5251 LamSF_Terms <> App constr
R5259:5261 Eta <> ref def
R5253:5256 SF_reduction <> k_op def
R5225:5236 Eta <> trans_etared constr
R5317:5318 Eta <> ap def
prf 5355:5358 <> eq_K
R5362:5372 Eta <> beta_eta_eq ind
R5379:5383 Eta <> abs_K def
R5374:5377 SF_reduction <> k_op def
R5417:5419 Coq.Init.Logic <> :type_scope:x_'='_x not
R5413:5416 SF_reduction <> k_op def
R5420:5427 LamSF_Terms <> lift_rec def
R5429:5432 SF_reduction <> k_op def
R5417:5419 Coq.Init.Logic <> :type_scope:x_'='_x not
R5413:5416 SF_reduction <> k_op def
R5420:5427 LamSF_Terms <> lift_rec def
R5429:5432 SF_reduction <> k_op def
R5456:5466 Eta <> beta_eta_eq ind
R5475:5477 Eta <> abs def
R5480:5481 Eta <> ap def
R5489:5491 Eta <> ref def
R5483:5486 SF_reduction <> k_op def
R5469:5472 SF_reduction <> k_op def
R5456:5466 Eta <> beta_eta_eq ind
R5475:5477 Eta <> abs def
R5480:5481 Eta <> ap def
R5489:5491 Eta <> ref def
R5483:5486 SF_reduction <> k_op def
R5469:5472 SF_reduction <> k_op def
R5546:5548 Coq.Init.Logic <> :type_scope:x_'='_x not
R5531:5532 Eta <> ap def
R5540:5542 Eta <> ref def
R5534:5537 SF_reduction <> k_op def
R5549:5556 LamSF_Terms <> lift_rec def
R5559:5560 Eta <> ap def
R5568:5570 Eta <> ref def
R5562:5565 SF_reduction <> k_op def
R5546:5548 Coq.Init.Logic <> :type_scope:x_'='_x not
R5531:5532 Eta <> ap def
R5540:5542 Eta <> ref def
R5534:5537 SF_reduction <> k_op def
R5549:5556 LamSF_Terms <> lift_rec def
R5559:5560 Eta <> ap def
R5568:5570 Eta <> ref def
R5562:5565 SF_reduction <> k_op def
R5598:5608 Eta <> beta_eta_eq ind
R5637:5639 Eta <> abs def
R5642:5644 Eta <> abs def
R5647:5648 Eta <> ap def
R5669:5671 Eta <> ref def
R5651:5652 Eta <> ap def
R5660:5662 Eta <> ref def
R5654:5657 SF_reduction <> k_op def
R5613:5615 Eta <> abs def
R5618:5619 Eta <> ap def
R5627:5629 Eta <> ref def
R5621:5624 SF_reduction <> k_op def
R5598:5608 Eta <> beta_eta_eq ind
R5637:5639 Eta <> abs def
R5642:5644 Eta <> abs def
R5647:5648 Eta <> ap def
R5669:5671 Eta <> ref def
R5651:5652 Eta <> ap def
R5660:5662 Eta <> ref def
R5654:5657 SF_reduction <> k_op def
R5613:5615 Eta <> abs def
R5618:5619 Eta <> ap def
R5627:5629 Eta <> ref def
R5621:5624 SF_reduction <> k_op def
R5708:5718 Eta <> beta_eta_eq ind
R5764:5766 Eta <> abs def
R5769:5771 Eta <> abs def
R5774:5776 Eta <> ref def
R5721:5723 Eta <> abs def
R5726:5728 Eta <> abs def
R5731:5732 Eta <> ap def
R5753:5755 Eta <> ref def
R5735:5736 Eta <> ap def
R5744:5746 Eta <> ref def
R5738:5741 SF_reduction <> k_op def
R5708:5718 Eta <> beta_eta_eq ind
R5764:5766 Eta <> abs def
R5769:5771 Eta <> abs def
R5774:5776 Eta <> ref def
R5721:5723 Eta <> abs def
R5726:5728 Eta <> abs def
R5731:5732 Eta <> ap def
R5753:5755 Eta <> ref def
R5735:5736 Eta <> ap def
R5744:5746 Eta <> ref def
R5738:5741 SF_reduction <> k_op def
R5793:5802 Eta <> abs_etared constr
R5813:5822 Eta <> abs_etared constr
R5833:5834 Eta <> ap def
R5837:5839 Eta <> ref def
prf 5881:5884 <> eq_S
R5888:5898 Eta <> beta_eta_eq ind
R5905:5909 Eta <> abs_S def
R5900:5903 SF_reduction <> s_op def
R5943:5945 Coq.Init.Logic <> :type_scope:x_'='_x not
R5939:5942 SF_reduction <> s_op def
R5946:5953 LamSF_Terms <> lift_rec def
R5955:5958 SF_reduction <> s_op def
R5943:5945 Coq.Init.Logic <> :type_scope:x_'='_x not
R5939:5942 SF_reduction <> s_op def
R5946:5953 LamSF_Terms <> lift_rec def
R5955:5958 SF_reduction <> s_op def
R5982:5992 Eta <> beta_eta_eq ind
R6001:6003 Eta <> abs def
R6006:6007 Eta <> ap def
R6015:6017 Eta <> ref def
R6009:6012 SF_reduction <> s_op def
R5995:5998 SF_reduction <> s_op def
R5982:5992 Eta <> beta_eta_eq ind
R6001:6003 Eta <> abs def
R6006:6007 Eta <> ap def
R6015:6017 Eta <> ref def
R6009:6012 SF_reduction <> s_op def
R5995:5998 SF_reduction <> s_op def
R6072:6074 Coq.Init.Logic <> :type_scope:x_'='_x not
R6057:6058 Eta <> ap def
R6066:6068 Eta <> ref def
R6060:6063 SF_reduction <> s_op def
R6075:6082 LamSF_Terms <> lift_rec def
R6085:6086 Eta <> ap def
R6094:6096 Eta <> ref def
R6088:6091 SF_reduction <> s_op def
R6072:6074 Coq.Init.Logic <> :type_scope:x_'='_x not
R6057:6058 Eta <> ap def
R6066:6068 Eta <> ref def
R6060:6063 SF_reduction <> s_op def
R6075:6082 LamSF_Terms <> lift_rec def
R6085:6086 Eta <> ap def
R6094:6096 Eta <> ref def
R6088:6091 SF_reduction <> s_op def
R6124:6134 Eta <> beta_eta_eq ind
R6163:6165 Eta <> abs def
R6168:6170 Eta <> abs def
R6173:6174 Eta <> ap def
R6195:6197 Eta <> ref def
R6177:6178 Eta <> ap def
R6186:6188 Eta <> ref def
R6180:6183 SF_reduction <> s_op def
R6139:6141 Eta <> abs def
R6144:6145 Eta <> ap def
R6153:6155 Eta <> ref def
R6147:6150 SF_reduction <> s_op def
R6124:6134 Eta <> beta_eta_eq ind
R6163:6165 Eta <> abs def
R6168:6170 Eta <> abs def
R6173:6174 Eta <> ap def
R6195:6197 Eta <> ref def
R6177:6178 Eta <> ap def
R6186:6188 Eta <> ref def
R6180:6183 SF_reduction <> s_op def
R6139:6141 Eta <> abs def
R6144:6145 Eta <> ap def
R6153:6155 Eta <> ref def
R6147:6150 SF_reduction <> s_op def
R6261:6263 Coq.Init.Logic <> :type_scope:x_'='_x not
R6234:6235 Eta <> ap def
R6255:6257 Eta <> ref def
R6238:6239 Eta <> ap def
R6247:6249 Eta <> ref def
R6241:6244 SF_reduction <> s_op def
R6264:6271 LamSF_Terms <> lift_rec def
R6274:6275 Eta <> ap def
R6296:6298 Eta <> ref def
R6278:6279 Eta <> ap def
R6287:6289 Eta <> ref def
R6281:6284 SF_reduction <> s_op def
R6261:6263 Coq.Init.Logic <> :type_scope:x_'='_x not
R6234:6235 Eta <> ap def
R6255:6257 Eta <> ref def
R6238:6239 Eta <> ap def
R6247:6249 Eta <> ref def
R6241:6244 SF_reduction <> s_op def
R6264:6271 LamSF_Terms <> lift_rec def
R6274:6275 Eta <> ap def
R6296:6298 Eta <> ref def
R6278:6279 Eta <> ap def
R6287:6289 Eta <> ref def
R6281:6284 SF_reduction <> s_op def
R6326:6336 Eta <> beta_eta_eq ind
R6382:6384 Eta <> abs def
R6387:6389 Eta <> abs def
R6392:6394 Eta <> abs def
R6397:6398 Eta <> ap def
R6432:6434 Eta <> ref def
R6401:6402 Eta <> ap def
R6423:6425 Eta <> ref def
R6405:6406 Eta <> ap def
R6414:6416 Eta <> ref def
R6408:6411 SF_reduction <> s_op def
R6339:6341 Eta <> abs def
R6344:6346 Eta <> abs def
R6349:6350 Eta <> ap def
R6371:6373 Eta <> ref def
R6353:6354 Eta <> ap def
R6362:6364 Eta <> ref def
R6356:6359 SF_reduction <> s_op def
R6326:6336 Eta <> beta_eta_eq ind
R6382:6384 Eta <> abs def
R6387:6389 Eta <> abs def
R6392:6394 Eta <> abs def
R6397:6398 Eta <> ap def
R6432:6434 Eta <> ref def
R6401:6402 Eta <> ap def
R6423:6425 Eta <> ref def
R6405:6406 Eta <> ap def
R6414:6416 Eta <> ref def
R6408:6411 SF_reduction <> s_op def
R6339:6341 Eta <> abs def
R6344:6346 Eta <> abs def
R6349:6350 Eta <> ap def
R6371:6373 Eta <> ref def
R6353:6354 Eta <> ap def
R6362:6364 Eta <> ref def
R6356:6359 SF_reduction <> s_op def
R6472:6482 Eta <> beta_eta_eq ind
R6546:6550 Eta <> abs_S def
R6485:6487 Eta <> abs def
R6490:6492 Eta <> abs def
R6495:6497 Eta <> abs def
R6500:6501 Eta <> ap def
R6535:6537 Eta <> ref def
R6504:6505 Eta <> ap def
R6526:6528 Eta <> ref def
R6508:6509 Eta <> ap def
R6517:6519 Eta <> ref def
R6511:6514 SF_reduction <> s_op def
R6472:6482 Eta <> beta_eta_eq ind
R6546:6550 Eta <> abs_S def
R6485:6487 Eta <> abs def
R6490:6492 Eta <> abs def
R6495:6497 Eta <> abs def
R6500:6501 Eta <> ap def
R6535:6537 Eta <> ref def
R6504:6505 Eta <> ap def
R6526:6528 Eta <> ref def
R6508:6509 Eta <> ap def
R6517:6519 Eta <> ref def
R6511:6514 SF_reduction <> s_op def
R6562:6566 Eta <> abs_S def
R6578:6587 Eta <> abs_etared constr
prf 6613:6626 <> star_equiv_abs
R6640:6650 Eta <> beta_eta_eq ind
R6662:6664 LamSF_Terms <> Abs constr
R6666:6666 Eta <> M var
R6653:6656 SF_reduction <> star def
R6658:6658 Eta <> M var
R6742:6745 Eta <> eq_I thm
R6783:6785 Eta <> abs def
R6788:6789 Eta <> ap def
R6826:6828 Eta <> ref def
R6792:6799 LamSF_Terms <> lift_rec def
R6802:6803 Eta <> ap def
R6811:6813 LamSF_Terms <> Ref constr
R6805:6808 SF_reduction <> k_op def
R6764:6775 Eta <> trans_etared constr
R6783:6785 Eta <> abs def
R6788:6789 Eta <> ap def
R6826:6828 Eta <> ref def
R6792:6799 LamSF_Terms <> lift_rec def
R6802:6803 Eta <> ap def
R6811:6813 LamSF_Terms <> Ref constr
R6805:6808 SF_reduction <> k_op def
R6764:6775 Eta <> trans_etared constr
R6866:6875 Eta <> abs_etared constr
R6932:6934 Eta <> abs def
R6937:6938 Eta <> ap def
R6973:6975 Eta <> ref def
R6941:6948 LamSF_Terms <> lift_rec def
R6951:6952 Eta <> ap def
R6960:6961 LamSF_Terms <> Op constr
R6954:6957 SF_reduction <> k_op def
R6913:6924 Eta <> trans_etared constr
R6932:6934 Eta <> abs def
R6937:6938 Eta <> ap def
R6973:6975 Eta <> ref def
R6941:6948 LamSF_Terms <> lift_rec def
R6951:6952 Eta <> ap def
R6960:6961 LamSF_Terms <> Op constr
R6954:6957 SF_reduction <> k_op def
R6913:6924 Eta <> trans_etared constr
R7006:7015 Eta <> abs_etared constr
R7052:7054 Eta <> abs def
R7057:7058 Eta <> ap def
R7109:7111 Eta <> ref def
R7061:7068 LamSF_Terms <> lift_rec def
R7071:7072 Eta <> ap def
R7094:7096 LamSF_Terms <> Abs constr
R7075:7076 Eta <> ap def
R7084:7086 LamSF_Terms <> Abs constr
R7078:7081 SF_reduction <> s_op def
R7033:7044 Eta <> trans_etared constr
R7052:7054 Eta <> abs def
R7057:7058 Eta <> ap def
R7109:7111 Eta <> ref def
R7061:7068 LamSF_Terms <> lift_rec def
R7071:7072 Eta <> ap def
R7094:7096 LamSF_Terms <> Abs constr
R7075:7076 Eta <> ap def
R7084:7086 LamSF_Terms <> Abs constr
R7078:7081 SF_reduction <> s_op def
R7033:7044 Eta <> trans_etared constr
R7134:7143 Eta <> abs_etared constr
R7179:7180 Eta <> ap def
R7221:7222 Eta <> ap def
R7249:7251 Eta <> ref def
R7225:7227 LamSF_Terms <> Abs constr
R7230:7237 LamSF_Terms <> lift_rec def
R7183:7184 Eta <> ap def
R7212:7214 Eta <> ref def
R7188:7190 LamSF_Terms <> Abs constr
R7193:7200 LamSF_Terms <> lift_rec def
R7160:7171 Eta <> trans_etared constr
R7179:7180 Eta <> ap def
R7221:7222 Eta <> ap def
R7249:7251 Eta <> ref def
R7225:7227 LamSF_Terms <> Abs constr
R7230:7237 LamSF_Terms <> lift_rec def
R7183:7184 Eta <> ap def
R7212:7214 Eta <> ref def
R7188:7190 LamSF_Terms <> Abs constr
R7193:7200 LamSF_Terms <> lift_rec def
R7160:7171 Eta <> trans_etared constr
R7275:7284 Eta <> app_etared constr
R7320:7324 LamSF_Terms <> subst def
R7335:7342 LamSF_Terms <> lift_rec def
R7327:7329 Eta <> ref def
R7301:7312 Eta <> trans_etared constr
R7320:7324 LamSF_Terms <> subst def
R7335:7342 LamSF_Terms <> lift_rec def
R7327:7329 Eta <> ref def
R7301:7312 Eta <> trans_etared constr
R7368:7372 LamSF_Terms <> subst def
R7383:7401 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7383:7401 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7383:7401 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7436:7440 LamSF_Terms <> subst def
R7451:7458 LamSF_Terms <> lift_rec def
R7443:7445 Eta <> ref def
R7417:7428 Eta <> trans_etared constr
R7436:7440 LamSF_Terms <> subst def
R7451:7458 LamSF_Terms <> lift_rec def
R7443:7445 Eta <> ref def
R7417:7428 Eta <> trans_etared constr
R7484:7488 LamSF_Terms <> subst def
R7499:7517 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7499:7517 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R7499:7517 LamSF_Substitution_term <> subst_rec_lift_rec2 thm