forked from Barry-Jay/lambdaSF
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Homomorphism.glob
1545 lines (1545 loc) · 57.9 KB
/
Homomorphism.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 b5fd3aa144c37c931cae047aacd66f06
FHomomorphism
R1992:1996 Coq.Arith.Arith <> <> lib
R2014:2016 Coq.Arith.Max <> <> lib
R2035:2038 Test <> <> lib
R2056:2062 General <> <> lib
R2081:2092 Lambda.Terms <> <> lib
R2110:2130 Lambda.Lambda_tactics <> <> lib
R2148:2171 Lambda.Substitution_term <> <> lib
R2189:2204 Lambda.Reduction <> <> lib
R2222:2235 Lambda.Redexes <> <> lib
R2253:2271 Lambda.Substitution <> <> lib
R2289:2304 Lambda.Residuals <> <> lib
R2322:2333 Lambda.Marks <> <> lib
R2351:2367 Lambda.Simulation <> <> lib
R2385:2395 Lambda.Cube <> <> lib
R2413:2429 Lambda.Confluence <> <> lib
R2447:2456 Lambda.Eta <> <> lib
R2474:2486 Lambda.Closed <> <> lib
R2504:2514 LamSF_Terms <> <> lib
R2532:2544 LamSF_Tactics <> <> lib
R2562:2584 LamSF_Substitution_term <> <> lib
R2602:2613 SF_reduction <> <> lib
R2631:2645 LamSF_reduction <> <> lib
R2663:2674 LamSF_Normal <> <> lib
R2692:2703 LamSF_Closed <> <> lib
R2721:2730 LamSF_Eval <> <> lib
R2748:2752 Coq.omega.Omega <> <> lib
def 2767:2769 <> ref
R2774:2782 Lambda.Terms <> Ref constr
def 2797:2798 <> ap
R2803:2811 Lambda.Terms <> App constr
def 2827:2829 <> abs
R2834:2842 Lambda.Terms <> Abs constr
def 2857:2861 <> abs_S
R2867:2869 Homomorphism <> abs def
R2872:2874 Homomorphism <> abs def
R2877:2879 Homomorphism <> abs def
R2882:2883 Homomorphism <> ap def
R2907:2908 Homomorphism <> ap def
R2919:2921 Homomorphism <> ref def
R2911:2913 Homomorphism <> ref def
R2886:2887 Homomorphism <> ap def
R2898:2900 Homomorphism <> ref def
R2890:2892 Homomorphism <> ref def
def 2945:2949 <> abs_K
R2955:2957 Homomorphism <> abs def
R2960:2962 Homomorphism <> abs def
R2965:2967 Homomorphism <> ref def
def 2986:2990 <> abs_I
R2996:2998 Homomorphism <> abs def
R3001:3003 Homomorphism <> ref def
def 3021:3026 <> abs_KI
R3032:3034 Homomorphism <> abs def
R3037:3039 Homomorphism <> abs def
R3042:3044 Homomorphism <> ref def
ind 3064:3075 <> homomorphism
constr 3110:3112 <> hom
R3078:3078 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3094:3098 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3084:3087 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3088:3093 Lambda.Terms <> lambda ind
R3079:3083 LamSF_Terms <> lamSF ind
R3132:3135 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3136:3141 Lambda.Terms <> lambda ind
R3127:3131 LamSF_Terms <> lamSF ind
R3147:3147 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3195:3202 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3203:3203 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3236:3243 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3244:3244 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3297:3305 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3306:3306 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3356:3362 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3363:3374 Homomorphism <> homomorphism ind
R3376:3376 Homomorphism <> h var
R3329:3332 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3352:3354 Coq.Init.Logic <> :type_scope:x_'='_x not
R3333:3345 Lambda.Closed <> maxvar def
R3348:3348 Homomorphism <> h var
R3350:3350 Homomorphism <> M var
R3325:3327 Coq.Init.Logic <> :type_scope:x_'='_x not
R3317:3322 LamSF_Closed <> maxvar def
R3324:3324 Homomorphism <> M var
R3270:3273 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3274:3284 Lambda.Eta <> beta_eta_eq ind
R3293:3293 Homomorphism <> h var
R3295:3295 Homomorphism <> N var
R3287:3287 Homomorphism <> h var
R3289:3289 Homomorphism <> M var
R3257:3265 LamSF_reduction <> lamSF_red def
R3269:3269 Homomorphism <> N var
R3267:3267 Homomorphism <> M var
R3222:3224 Coq.Init.Logic <> :type_scope:x_'='_x not
R3214:3214 Homomorphism <> h var
R3216:3218 LamSF_Terms <> Ref constr
R3220:3220 Homomorphism <> n var
R3225:3233 Lambda.Terms <> Ref constr
R3235:3235 Homomorphism <> n var
R3171:3173 Coq.Init.Logic <> :type_scope:x_'='_x not
R3160:3160 Homomorphism <> h var
R3163:3165 LamSF_Terms <> App constr
R3169:3169 Homomorphism <> N var
R3167:3167 Homomorphism <> M var
R3174:3182 Lambda.Terms <> App constr
R3191:3191 Homomorphism <> h var
R3193:3193 Homomorphism <> N var
R3185:3185 Homomorphism <> h var
R3187:3187 Homomorphism <> M var
prf 3388:3401 <> homomorphism_I
R3429:3432 Coq.Init.Logic <> :type_scope:x_'->'_x not
R3433:3443 Lambda.Eta <> beta_eta_eq ind
R3454:3458 Homomorphism <> abs_I def
R3446:3446 Homomorphism <> h var
R3448:3451 SF_reduction <> i_op def
R3415:3426 Homomorphism <> homomorphism ind
R3428:3428 Homomorphism <> h var
R3540:3542 Coq.Init.Logic <> :type_scope:x_'='_x not
R3519:3531 Lambda.Closed <> maxvar def
R3535:3538 SF_reduction <> i_op def
R3540:3542 Coq.Init.Logic <> :type_scope:x_'='_x not
R3519:3531 Lambda.Closed <> maxvar def
R3535:3538 SF_reduction <> i_op def
R3606:3608 Coq.Init.Logic <> :type_scope:x_'='_x not
R3579:3592 Lambda.Terms <> lift_rec def
R3605:3605 Homomorphism <> k var
R3597:3600 SF_reduction <> i_op def
R3611:3614 SF_reduction <> i_op def
R3606:3608 Coq.Init.Logic <> :type_scope:x_'='_x not
R3579:3592 Lambda.Terms <> lift_rec def
R3605:3605 Homomorphism <> k var
R3597:3600 SF_reduction <> i_op def
R3611:3614 SF_reduction <> i_op def
R3627:3648 Lambda.Closed <> lift_rec_closed thm
R3667:3674 Lambda.Eta <> beta_eta def
R3708:3711 SF_reduction <> i_op def
R3678:3680 Homomorphism <> abs def
R3683:3684 Homomorphism <> ap def
R3696:3698 Homomorphism <> ref def
R3689:3692 SF_reduction <> i_op def
R3667:3674 Lambda.Eta <> beta_eta def
R3708:3711 SF_reduction <> i_op def
R3678:3680 Homomorphism <> abs def
R3683:3684 Homomorphism <> ap def
R3696:3698 Homomorphism <> ref def
R3689:3692 SF_reduction <> i_op def
R3724:3731 Lambda.Eta <> beta_eta def
R3796:3798 Homomorphism <> abs def
R3801:3802 Homomorphism <> ap def
R3814:3816 Homomorphism <> ref def
R3807:3810 SF_reduction <> i_op def
R3766:3787 Lambda.Lambda_tactics <> seq_red constr
R3796:3798 Homomorphism <> abs def
R3801:3802 Homomorphism <> ap def
R3814:3816 Homomorphism <> ref def
R3807:3810 SF_reduction <> i_op def
R3766:3787 Lambda.Lambda_tactics <> seq_red constr
R3838:3840 Homomorphism <> abs def
R3843:3844 Homomorphism <> ap def
R3895:3902 Lambda.Eta <> beta_eta def
R3951:3953 Homomorphism <> abs def
R3959:3961 LamSF_Terms <> App constr
R3969:3971 LamSF_Terms <> Ref constr
R3963:3966 SF_reduction <> i_op def
R3914:3916 Homomorphism <> abs def
R3919:3920 Homomorphism <> ap def
R3932:3934 Homomorphism <> ref def
R3925:3928 SF_reduction <> i_op def
R3895:3902 Lambda.Eta <> beta_eta def
R3951:3953 Homomorphism <> abs def
R3959:3961 LamSF_Terms <> App constr
R3969:3971 LamSF_Terms <> Ref constr
R3963:3966 SF_reduction <> i_op def
R3914:3916 Homomorphism <> abs def
R3919:3920 Homomorphism <> ap def
R3932:3934 Homomorphism <> ref def
R3925:3928 SF_reduction <> i_op def
R3998:4019 Lambda.Eta <> preserves_abs_beta_eta thm
R3998:4019 Lambda.Eta <> preserves_abs_beta_eta thm
R4082:4104 Lambda.Lambda_tactics <> zero_red constr
R4133:4148 Lambda.Eta <> diamond_beta_eta thm
R4201:4203 Homomorphism <> abs def
R4209:4211 LamSF_Terms <> App constr
R4219:4221 LamSF_Terms <> Ref constr
R4213:4216 SF_reduction <> i_op def
R4191:4194 SF_reduction <> i_op def
R4152:4154 Homomorphism <> abs def
R4157:4158 Homomorphism <> ap def
R4170:4172 Homomorphism <> ref def
R4163:4166 SF_reduction <> i_op def
R4133:4148 Lambda.Eta <> diamond_beta_eta thm
R4201:4203 Homomorphism <> abs def
R4209:4211 LamSF_Terms <> App constr
R4219:4221 LamSF_Terms <> Ref constr
R4213:4216 SF_reduction <> i_op def
R4191:4194 SF_reduction <> i_op def
R4152:4154 Homomorphism <> abs def
R4157:4158 Homomorphism <> ap def
R4170:4172 Homomorphism <> ref def
R4163:4166 SF_reduction <> i_op def
R4250:4260 Lambda.Eta <> beta_eta_eq ind
R4285:4287 Homomorphism <> abs def
R4293:4295 LamSF_Terms <> App constr
R4303:4305 LamSF_Terms <> Ref constr
R4297:4300 SF_reduction <> i_op def
R4266:4269 SF_reduction <> i_op def
R4250:4260 Lambda.Eta <> beta_eta_eq ind
R4285:4287 Homomorphism <> abs def
R4293:4295 LamSF_Terms <> App constr
R4303:4305 LamSF_Terms <> Ref constr
R4297:4300 SF_reduction <> i_op def
R4266:4269 SF_reduction <> i_op def
R4324:4336 Lambda.Eta <> common_reduct constr
R4367:4377 Lambda.Eta <> beta_eta_eq ind
R4423:4427 Homomorphism <> abs_I def
R4394:4396 Homomorphism <> abs def
R4402:4404 LamSF_Terms <> App constr
R4412:4414 LamSF_Terms <> Ref constr
R4406:4409 SF_reduction <> i_op def
R4367:4377 Lambda.Eta <> beta_eta_eq ind
R4423:4427 Homomorphism <> abs_I def
R4394:4396 Homomorphism <> abs def
R4402:4404 LamSF_Terms <> App constr
R4412:4414 LamSF_Terms <> Ref constr
R4406:4409 SF_reduction <> i_op def
R4439:4443 Homomorphism <> abs_I def
R4463:4487 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R4463:4487 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R4530:4532 LamSF_Terms <> App constr
R4554:4556 LamSF_Terms <> App constr
R4564:4566 LamSF_Terms <> Ref constr
R4558:4561 SF_reduction <> k_op def
R4535:4537 LamSF_Terms <> App constr
R4545:4547 LamSF_Terms <> Ref constr
R4539:4542 SF_reduction <> k_op def
R4498:4519 Lambda.Eta <> beta_eta_eq_transitive thm
R4530:4532 LamSF_Terms <> App constr
R4554:4556 LamSF_Terms <> App constr
R4564:4566 LamSF_Terms <> Ref constr
R4558:4561 SF_reduction <> k_op def
R4535:4537 LamSF_Terms <> App constr
R4545:4547 LamSF_Terms <> Ref constr
R4539:4542 SF_reduction <> k_op def
R4498:4519 Lambda.Eta <> beta_eta_eq_transitive thm
R4644:4646 LamSF_Terms <> Ref constr
R4612:4633 Lambda.Eta <> beta_eta_eq_transitive thm
R4644:4646 LamSF_Terms <> Ref constr
R4612:4633 Lambda.Eta <> beta_eta_eq_transitive thm
R4734:4735 Homomorphism <> ap def
R4738:4740 Homomorphism <> ref def
R4760:4781 Lambda.Eta <> beta_eta_eq_transitive thm
prf 4805:4818 <> homomorphism_K
R4846:4849 Coq.Init.Logic <> :type_scope:x_'->'_x not
R4850:4860 Lambda.Eta <> beta_eta_eq ind
R4871:4875 Homomorphism <> abs_K def
R4863:4863 Homomorphism <> h var
R4865:4868 SF_reduction <> k_op def
R4832:4843 Homomorphism <> homomorphism ind
R4845:4845 Homomorphism <> h var
R4957:4959 Coq.Init.Logic <> :type_scope:x_'='_x not
R4936:4948 Lambda.Closed <> maxvar def
R4952:4955 SF_reduction <> k_op def
R4957:4959 Coq.Init.Logic <> :type_scope:x_'='_x not
R4936:4948 Lambda.Closed <> maxvar def
R4952:4955 SF_reduction <> k_op def
R5023:5025 Coq.Init.Logic <> :type_scope:x_'='_x not
R4996:5009 Lambda.Terms <> lift_rec def
R5022:5022 Homomorphism <> k var
R5014:5017 SF_reduction <> k_op def
R5028:5031 SF_reduction <> k_op def
R5023:5025 Coq.Init.Logic <> :type_scope:x_'='_x not
R4996:5009 Lambda.Terms <> lift_rec def
R5022:5022 Homomorphism <> k var
R5014:5017 SF_reduction <> k_op def
R5028:5031 SF_reduction <> k_op def
R5044:5065 Lambda.Closed <> lift_rec_closed thm
R5084:5091 Lambda.Eta <> beta_eta def
R5144:5147 SF_reduction <> k_op def
R5095:5097 Homomorphism <> abs def
R5100:5102 Homomorphism <> abs def
R5105:5106 Homomorphism <> ap def
R5131:5133 Homomorphism <> ref def
R5109:5110 Homomorphism <> ap def
R5122:5124 Homomorphism <> ref def
R5115:5118 SF_reduction <> k_op def
R5084:5091 Lambda.Eta <> beta_eta def
R5144:5147 SF_reduction <> k_op def
R5095:5097 Homomorphism <> abs def
R5100:5102 Homomorphism <> abs def
R5105:5106 Homomorphism <> ap def
R5131:5133 Homomorphism <> ref def
R5109:5110 Homomorphism <> ap def
R5122:5124 Homomorphism <> ref def
R5115:5118 SF_reduction <> k_op def
R5189:5191 Homomorphism <> abs def
R5194:5195 Homomorphism <> ap def
R5207:5209 Homomorphism <> ref def
R5200:5203 SF_reduction <> k_op def
R5159:5181 Lambda.Lambda_tactics <> succ_red constr
R5189:5191 Homomorphism <> abs def
R5194:5195 Homomorphism <> ap def
R5207:5209 Homomorphism <> ref def
R5200:5203 SF_reduction <> k_op def
R5159:5181 Lambda.Lambda_tactics <> succ_red constr
R5225:5233 Lambda.Eta <> beta_eta1 def
R5272:5274 Homomorphism <> abs def
R5277:5279 Homomorphism <> abs def
R5282:5283 Homomorphism <> ap def
R5308:5310 Homomorphism <> ref def
R5286:5287 Homomorphism <> ap def
R5299:5301 Homomorphism <> ref def
R5292:5295 SF_reduction <> k_op def
R5243:5264 Lambda.Lambda_tactics <> seq_red constr
R5272:5274 Homomorphism <> abs def
R5277:5279 Homomorphism <> abs def
R5282:5283 Homomorphism <> ap def
R5308:5310 Homomorphism <> ref def
R5286:5287 Homomorphism <> ap def
R5299:5301 Homomorphism <> ref def
R5292:5295 SF_reduction <> k_op def
R5243:5264 Lambda.Lambda_tactics <> seq_red constr
R5333:5335 Homomorphism <> abs def
R5338:5339 Homomorphism <> ap def
R5357:5366 Lambda.Eta <> abs_etared constr
R5379:5387 Lambda.Terms <> App constr
R5398:5400 Homomorphism <> ref def
R5392:5395 SF_reduction <> k_op def
R5412:5425 Lambda.Terms <> lift_rec def
R5428:5429 Homomorphism <> ap def
R5441:5443 Homomorphism <> ref def
R5434:5437 SF_reduction <> k_op def
R5379:5387 Lambda.Terms <> App constr
R5398:5400 Homomorphism <> ref def
R5392:5395 SF_reduction <> k_op def
R5412:5425 Lambda.Terms <> lift_rec def
R5428:5429 Homomorphism <> ap def
R5441:5443 Homomorphism <> ref def
R5434:5437 SF_reduction <> k_op def
R5463:5469 Lambda.Eta <> eta_red constr
R5483:5485 Homomorphism <> abs def
R5488:5489 Homomorphism <> ap def
R5617:5619 Homomorphism <> abs def
R5622:5623 Homomorphism <> ap def
R5635:5637 Homomorphism <> ref def
R5628:5631 SF_reduction <> k_op def
R5587:5608 Lambda.Lambda_tactics <> seq_red constr
R5617:5619 Homomorphism <> abs def
R5622:5623 Homomorphism <> ap def
R5635:5637 Homomorphism <> ref def
R5628:5631 SF_reduction <> k_op def
R5587:5608 Lambda.Lambda_tactics <> seq_red constr
R5659:5661 Homomorphism <> abs def
R5664:5665 Homomorphism <> ap def
R5716:5723 Lambda.Eta <> beta_eta def
R5791:5793 Homomorphism <> abs def
R5796:5798 Homomorphism <> abs def
R5804:5806 LamSF_Terms <> App constr
R5828:5830 LamSF_Terms <> Ref constr
R5809:5811 LamSF_Terms <> App constr
R5819:5821 LamSF_Terms <> Ref constr
R5813:5816 SF_reduction <> k_op def
R5735:5737 Homomorphism <> abs def
R5740:5742 Homomorphism <> abs def
R5745:5746 Homomorphism <> ap def
R5771:5773 Homomorphism <> ref def
R5749:5750 Homomorphism <> ap def
R5762:5764 Homomorphism <> ref def
R5755:5758 SF_reduction <> k_op def
R5716:5723 Lambda.Eta <> beta_eta def
R5791:5793 Homomorphism <> abs def
R5796:5798 Homomorphism <> abs def
R5804:5806 LamSF_Terms <> App constr
R5828:5830 LamSF_Terms <> Ref constr
R5809:5811 LamSF_Terms <> App constr
R5819:5821 LamSF_Terms <> Ref constr
R5813:5816 SF_reduction <> k_op def
R5735:5737 Homomorphism <> abs def
R5740:5742 Homomorphism <> abs def
R5745:5746 Homomorphism <> ap def
R5771:5773 Homomorphism <> ref def
R5749:5750 Homomorphism <> ap def
R5762:5764 Homomorphism <> ref def
R5755:5758 SF_reduction <> k_op def
R5858:5879 Lambda.Eta <> preserves_abs_beta_eta thm
R5858:5879 Lambda.Eta <> preserves_abs_beta_eta thm
R5858:5879 Lambda.Eta <> preserves_abs_beta_eta thm
R5942:5964 Lambda.Lambda_tactics <> zero_red constr
R5993:6008 Lambda.Eta <> diamond_beta_eta thm
R6093:6095 Homomorphism <> abs def
R6098:6100 Homomorphism <> abs def
R6106:6108 LamSF_Terms <> App constr
R6131:6133 LamSF_Terms <> Ref constr
R6111:6113 LamSF_Terms <> App constr
R6122:6124 LamSF_Terms <> Ref constr
R6115:6118 SF_reduction <> k_op def
R6070:6073 SF_reduction <> k_op def
R6012:6014 Homomorphism <> abs def
R6017:6019 Homomorphism <> abs def
R6022:6023 Homomorphism <> ap def
R6048:6050 Homomorphism <> ref def
R6026:6027 Homomorphism <> ap def
R6039:6041 Homomorphism <> ref def
R6032:6035 SF_reduction <> k_op def
R5993:6008 Lambda.Eta <> diamond_beta_eta thm
R6093:6095 Homomorphism <> abs def
R6098:6100 Homomorphism <> abs def
R6106:6108 LamSF_Terms <> App constr
R6131:6133 LamSF_Terms <> Ref constr
R6111:6113 LamSF_Terms <> App constr
R6122:6124 LamSF_Terms <> Ref constr
R6115:6118 SF_reduction <> k_op def
R6070:6073 SF_reduction <> k_op def
R6012:6014 Homomorphism <> abs def
R6017:6019 Homomorphism <> abs def
R6022:6023 Homomorphism <> ap def
R6048:6050 Homomorphism <> ref def
R6026:6027 Homomorphism <> ap def
R6039:6041 Homomorphism <> ref def
R6032:6035 SF_reduction <> k_op def
R6163:6173 Lambda.Eta <> beta_eta_eq ind
R6198:6200 Homomorphism <> abs def
R6203:6205 Homomorphism <> abs def
R6211:6213 LamSF_Terms <> App constr
R6235:6237 LamSF_Terms <> Ref constr
R6216:6218 LamSF_Terms <> App constr
R6226:6228 LamSF_Terms <> Ref constr
R6220:6223 SF_reduction <> k_op def
R6179:6182 SF_reduction <> k_op def
R6163:6173 Lambda.Eta <> beta_eta_eq ind
R6198:6200 Homomorphism <> abs def
R6203:6205 Homomorphism <> abs def
R6211:6213 LamSF_Terms <> App constr
R6235:6237 LamSF_Terms <> Ref constr
R6216:6218 LamSF_Terms <> App constr
R6226:6228 LamSF_Terms <> Ref constr
R6220:6223 SF_reduction <> k_op def
R6179:6182 SF_reduction <> k_op def
R6257:6269 Lambda.Eta <> common_reduct constr
R6300:6310 Lambda.Eta <> beta_eta_eq ind
R6376:6380 Homomorphism <> abs_K def
R6327:6329 Homomorphism <> abs def
R6332:6334 Homomorphism <> abs def
R6340:6342 LamSF_Terms <> App constr
R6364:6366 LamSF_Terms <> Ref constr
R6345:6347 LamSF_Terms <> App constr
R6355:6357 LamSF_Terms <> Ref constr
R6349:6352 SF_reduction <> k_op def
R6300:6310 Lambda.Eta <> beta_eta_eq ind
R6376:6380 Homomorphism <> abs_K def
R6327:6329 Homomorphism <> abs def
R6332:6334 Homomorphism <> abs def
R6340:6342 LamSF_Terms <> App constr
R6364:6366 LamSF_Terms <> Ref constr
R6345:6347 LamSF_Terms <> App constr
R6355:6357 LamSF_Terms <> Ref constr
R6349:6352 SF_reduction <> k_op def
R6392:6396 Homomorphism <> abs_K def
R6416:6440 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R6416:6440 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R6416:6440 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R6483:6485 LamSF_Terms <> Ref constr
R6451:6472 Lambda.Eta <> beta_eta_eq_transitive thm
R6483:6485 LamSF_Terms <> Ref constr
R6451:6472 Lambda.Eta <> beta_eta_eq_transitive thm
R6573:6574 Homomorphism <> ap def
R6577:6579 Homomorphism <> ref def
R6599:6620 Lambda.Eta <> beta_eta_eq_transitive thm
prf 6645:6659 <> homomorphism_KI
R6687:6690 Coq.Init.Logic <> :type_scope:x_'->'_x not
R6691:6701 Lambda.Eta <> beta_eta_eq ind
R6723:6728 Homomorphism <> abs_KI def
R6704:6704 Homomorphism <> h var
R6707:6709 LamSF_Terms <> App constr
R6716:6719 SF_reduction <> i_op def
R6711:6714 SF_reduction <> k_op def
R6673:6684 Homomorphism <> homomorphism ind
R6686:6686 Homomorphism <> h var
R6822:6824 Coq.Init.Logic <> :type_scope:x_'='_x not
R6789:6801 Lambda.Closed <> maxvar def
R6807:6809 LamSF_Terms <> App constr
R6816:6819 SF_reduction <> i_op def
R6811:6814 SF_reduction <> k_op def
R6822:6824 Coq.Init.Logic <> :type_scope:x_'='_x not
R6789:6801 Lambda.Closed <> maxvar def
R6807:6809 LamSF_Terms <> App constr
R6816:6819 SF_reduction <> i_op def
R6811:6814 SF_reduction <> k_op def
R6899:6901 Coq.Init.Logic <> :type_scope:x_'='_x not
R6861:6874 Lambda.Terms <> lift_rec def
R6898:6898 Homomorphism <> k var
R6880:6882 LamSF_Terms <> App constr
R6889:6892 SF_reduction <> i_op def
R6884:6887 SF_reduction <> k_op def
R6905:6907 LamSF_Terms <> App constr
R6914:6917 SF_reduction <> i_op def
R6909:6912 SF_reduction <> k_op def
R6899:6901 Coq.Init.Logic <> :type_scope:x_'='_x not
R6861:6874 Lambda.Terms <> lift_rec def
R6898:6898 Homomorphism <> k var
R6880:6882 LamSF_Terms <> App constr
R6889:6892 SF_reduction <> i_op def
R6884:6887 SF_reduction <> k_op def
R6905:6907 LamSF_Terms <> App constr
R6914:6917 SF_reduction <> i_op def
R6909:6912 SF_reduction <> k_op def
R6931:6952 Lambda.Closed <> lift_rec_closed thm
R6971:6978 Lambda.Eta <> beta_eta def
R7043:7045 LamSF_Terms <> App constr
R7052:7055 SF_reduction <> i_op def
R7047:7050 SF_reduction <> k_op def
R6982:6984 Homomorphism <> abs def
R6987:6989 Homomorphism <> abs def
R6992:6993 Homomorphism <> ap def
R7029:7031 Homomorphism <> ref def
R6996:6997 Homomorphism <> ap def
R7020:7022 Homomorphism <> ref def
R7003:7005 LamSF_Terms <> App constr
R7012:7015 SF_reduction <> i_op def
R7007:7010 SF_reduction <> k_op def
R6971:6978 Lambda.Eta <> beta_eta def
R7043:7045 LamSF_Terms <> App constr
R7052:7055 SF_reduction <> i_op def
R7047:7050 SF_reduction <> k_op def
R6982:6984 Homomorphism <> abs def
R6987:6989 Homomorphism <> abs def
R6992:6993 Homomorphism <> ap def
R7029:7031 Homomorphism <> ref def
R6996:6997 Homomorphism <> ap def
R7020:7022 Homomorphism <> ref def
R7003:7005 LamSF_Terms <> App constr
R7012:7015 SF_reduction <> i_op def
R7007:7010 SF_reduction <> k_op def
R7098:7100 Homomorphism <> abs def
R7103:7104 Homomorphism <> ap def
R7127:7129 Homomorphism <> ref def
R7110:7112 LamSF_Terms <> App constr
R7119:7122 SF_reduction <> i_op def
R7114:7117 SF_reduction <> k_op def
R7068:7090 Lambda.Lambda_tactics <> succ_red constr
R7098:7100 Homomorphism <> abs def
R7103:7104 Homomorphism <> ap def
R7127:7129 Homomorphism <> ref def
R7110:7112 LamSF_Terms <> App constr
R7119:7122 SF_reduction <> i_op def
R7114:7117 SF_reduction <> k_op def
R7068:7090 Lambda.Lambda_tactics <> succ_red constr
R7145:7153 Lambda.Eta <> beta_eta1 def
R7192:7194 Homomorphism <> abs def
R7197:7199 Homomorphism <> abs def
R7202:7203 Homomorphism <> ap def
R7239:7241 Homomorphism <> ref def
R7206:7207 Homomorphism <> ap def
R7230:7232 Homomorphism <> ref def
R7213:7215 LamSF_Terms <> App constr
R7222:7225 SF_reduction <> i_op def
R7217:7220 SF_reduction <> k_op def
R7163:7184 Lambda.Lambda_tactics <> seq_red constr
R7192:7194 Homomorphism <> abs def
R7197:7199 Homomorphism <> abs def
R7202:7203 Homomorphism <> ap def
R7239:7241 Homomorphism <> ref def
R7206:7207 Homomorphism <> ap def
R7230:7232 Homomorphism <> ref def
R7213:7215 LamSF_Terms <> App constr
R7222:7225 SF_reduction <> i_op def
R7217:7220 SF_reduction <> k_op def
R7163:7184 Lambda.Lambda_tactics <> seq_red constr
R7264:7266 Homomorphism <> abs def
R7269:7270 Homomorphism <> ap def
R7288:7297 Lambda.Eta <> abs_etared constr
R7310:7318 Lambda.Terms <> App constr
R7340:7342 Homomorphism <> ref def
R7324:7326 LamSF_Terms <> App constr
R7333:7336 SF_reduction <> i_op def
R7328:7331 SF_reduction <> k_op def
R7354:7367 Lambda.Terms <> lift_rec def
R7370:7371 Homomorphism <> ap def
R7394:7396 Homomorphism <> ref def
R7377:7379 LamSF_Terms <> App constr
R7386:7389 SF_reduction <> i_op def
R7381:7384 SF_reduction <> k_op def
R7310:7318 Lambda.Terms <> App constr
R7340:7342 Homomorphism <> ref def
R7324:7326 LamSF_Terms <> App constr
R7333:7336 SF_reduction <> i_op def
R7328:7331 SF_reduction <> k_op def
R7354:7367 Lambda.Terms <> lift_rec def
R7370:7371 Homomorphism <> ap def
R7394:7396 Homomorphism <> ref def
R7377:7379 LamSF_Terms <> App constr
R7386:7389 SF_reduction <> i_op def
R7381:7384 SF_reduction <> k_op def
R7416:7422 Lambda.Eta <> eta_red constr
R7436:7438 Homomorphism <> abs def
R7441:7442 Homomorphism <> ap def
R7570:7572 Homomorphism <> abs def
R7575:7576 Homomorphism <> ap def
R7599:7601 Homomorphism <> ref def
R7582:7584 LamSF_Terms <> App constr
R7591:7594 SF_reduction <> i_op def
R7586:7589 SF_reduction <> k_op def
R7540:7561 Lambda.Lambda_tactics <> seq_red constr
R7570:7572 Homomorphism <> abs def
R7575:7576 Homomorphism <> ap def
R7599:7601 Homomorphism <> ref def
R7582:7584 LamSF_Terms <> App constr
R7591:7594 SF_reduction <> i_op def
R7586:7589 SF_reduction <> k_op def
R7540:7561 Lambda.Lambda_tactics <> seq_red constr
R7623:7625 Homomorphism <> abs def
R7628:7629 Homomorphism <> ap def
R7680:7687 Lambda.Eta <> beta_eta def
R7766:7768 Homomorphism <> abs def
R7771:7773 Homomorphism <> abs def
R7779:7781 LamSF_Terms <> App constr
R7814:7816 LamSF_Terms <> Ref constr
R7784:7786 LamSF_Terms <> App constr
R7805:7807 LamSF_Terms <> Ref constr
R7789:7791 LamSF_Terms <> App constr
R7798:7801 SF_reduction <> i_op def
R7793:7796 SF_reduction <> k_op def
R7699:7701 Homomorphism <> abs def
R7704:7706 Homomorphism <> abs def
R7709:7710 Homomorphism <> ap def
R7746:7748 Homomorphism <> ref def
R7713:7714 Homomorphism <> ap def
R7737:7739 Homomorphism <> ref def
R7720:7722 LamSF_Terms <> App constr
R7729:7732 SF_reduction <> i_op def
R7724:7727 SF_reduction <> k_op def
R7680:7687 Lambda.Eta <> beta_eta def
R7766:7768 Homomorphism <> abs def
R7771:7773 Homomorphism <> abs def
R7779:7781 LamSF_Terms <> App constr
R7814:7816 LamSF_Terms <> Ref constr
R7784:7786 LamSF_Terms <> App constr
R7805:7807 LamSF_Terms <> Ref constr
R7789:7791 LamSF_Terms <> App constr
R7798:7801 SF_reduction <> i_op def
R7793:7796 SF_reduction <> k_op def
R7699:7701 Homomorphism <> abs def
R7704:7706 Homomorphism <> abs def
R7709:7710 Homomorphism <> ap def
R7746:7748 Homomorphism <> ref def
R7713:7714 Homomorphism <> ap def
R7737:7739 Homomorphism <> ref def
R7720:7722 LamSF_Terms <> App constr
R7729:7732 SF_reduction <> i_op def
R7724:7727 SF_reduction <> k_op def
R7844:7865 Lambda.Eta <> preserves_abs_beta_eta thm
R7844:7865 Lambda.Eta <> preserves_abs_beta_eta thm
R7844:7865 Lambda.Eta <> preserves_abs_beta_eta thm
R7928:7950 Lambda.Lambda_tactics <> zero_red constr
R7979:7994 Lambda.Eta <> diamond_beta_eta thm
R8101:8103 Homomorphism <> abs def
R8106:8108 Homomorphism <> abs def
R8114:8116 LamSF_Terms <> App constr
R8150:8152 LamSF_Terms <> Ref constr
R8119:8121 LamSF_Terms <> App constr
R8141:8143 LamSF_Terms <> Ref constr
R8124:8126 LamSF_Terms <> App constr
R8133:8136 SF_reduction <> i_op def
R8128:8131 SF_reduction <> k_op def
R8068:8070 LamSF_Terms <> App constr
R8077:8080 SF_reduction <> i_op def
R8072:8075 SF_reduction <> k_op def
R7998:8000 Homomorphism <> abs def
R8003:8005 Homomorphism <> abs def
R8008:8009 Homomorphism <> ap def
R8045:8047 Homomorphism <> ref def
R8012:8013 Homomorphism <> ap def
R8036:8038 Homomorphism <> ref def
R8019:8021 LamSF_Terms <> App constr
R8028:8031 SF_reduction <> i_op def
R8023:8026 SF_reduction <> k_op def
R7979:7994 Lambda.Eta <> diamond_beta_eta thm
R8101:8103 Homomorphism <> abs def
R8106:8108 Homomorphism <> abs def
R8114:8116 LamSF_Terms <> App constr
R8150:8152 LamSF_Terms <> Ref constr
R8119:8121 LamSF_Terms <> App constr
R8141:8143 LamSF_Terms <> Ref constr
R8124:8126 LamSF_Terms <> App constr
R8133:8136 SF_reduction <> i_op def
R8128:8131 SF_reduction <> k_op def
R8068:8070 LamSF_Terms <> App constr
R8077:8080 SF_reduction <> i_op def
R8072:8075 SF_reduction <> k_op def
R7998:8000 Homomorphism <> abs def
R8003:8005 Homomorphism <> abs def
R8008:8009 Homomorphism <> ap def
R8045:8047 Homomorphism <> ref def
R8012:8013 Homomorphism <> ap def
R8036:8038 Homomorphism <> ref def
R8019:8021 LamSF_Terms <> App constr
R8028:8031 SF_reduction <> i_op def
R8023:8026 SF_reduction <> k_op def
R8182:8192 Lambda.Eta <> beta_eta_eq ind
R8228:8230 Homomorphism <> abs def
R8233:8235 Homomorphism <> abs def
R8241:8243 LamSF_Terms <> App constr
R8276:8278 LamSF_Terms <> Ref constr
R8246:8248 LamSF_Terms <> App constr
R8267:8269 LamSF_Terms <> Ref constr
R8251:8253 LamSF_Terms <> App constr
R8260:8263 SF_reduction <> i_op def
R8255:8258 SF_reduction <> k_op def
R8199:8201 LamSF_Terms <> App constr
R8208:8211 SF_reduction <> i_op def
R8203:8206 SF_reduction <> k_op def
R8182:8192 Lambda.Eta <> beta_eta_eq ind
R8228:8230 Homomorphism <> abs def
R8233:8235 Homomorphism <> abs def
R8241:8243 LamSF_Terms <> App constr
R8276:8278 LamSF_Terms <> Ref constr
R8246:8248 LamSF_Terms <> App constr
R8267:8269 LamSF_Terms <> Ref constr
R8251:8253 LamSF_Terms <> App constr
R8260:8263 SF_reduction <> i_op def
R8255:8258 SF_reduction <> k_op def
R8199:8201 LamSF_Terms <> App constr
R8208:8211 SF_reduction <> i_op def
R8203:8206 SF_reduction <> k_op def
R8298:8310 Lambda.Eta <> common_reduct constr
R8341:8351 Lambda.Eta <> beta_eta_eq ind
R8428:8433 Homomorphism <> abs_KI def
R8368:8370 Homomorphism <> abs def
R8373:8375 Homomorphism <> abs def
R8381:8383 LamSF_Terms <> App constr
R8416:8418 LamSF_Terms <> Ref constr
R8386:8388 LamSF_Terms <> App constr
R8407:8409 LamSF_Terms <> Ref constr
R8391:8393 LamSF_Terms <> App constr
R8400:8403 SF_reduction <> i_op def
R8395:8398 SF_reduction <> k_op def
R8341:8351 Lambda.Eta <> beta_eta_eq ind
R8428:8433 Homomorphism <> abs_KI def
R8368:8370 Homomorphism <> abs def
R8373:8375 Homomorphism <> abs def
R8381:8383 LamSF_Terms <> App constr
R8416:8418 LamSF_Terms <> Ref constr
R8386:8388 LamSF_Terms <> App constr
R8407:8409 LamSF_Terms <> Ref constr
R8391:8393 LamSF_Terms <> App constr
R8400:8403 SF_reduction <> i_op def
R8395:8398 SF_reduction <> k_op def
R8445:8450 Homomorphism <> abs_KI def
R8470:8494 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R8470:8494 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R8470:8494 Lambda.Eta <> preserves_abs_beta_eta_eq thm
R8537:8539 LamSF_Terms <> App constr
R8547:8549 LamSF_Terms <> Ref constr
R8541:8544 SF_reduction <> i_op def
R8505:8526 Lambda.Eta <> beta_eta_eq_transitive thm
R8537:8539 LamSF_Terms <> App constr
R8547:8549 LamSF_Terms <> Ref constr
R8541:8544 SF_reduction <> i_op def
R8505:8526 Lambda.Eta <> beta_eta_eq_transitive thm
R8626:8628 LamSF_Terms <> App constr
R8650:8652 LamSF_Terms <> App constr
R8660:8662 LamSF_Terms <> Ref constr
R8654:8657 SF_reduction <> k_op def
R8631:8633 LamSF_Terms <> App constr
R8641:8643 LamSF_Terms <> Ref constr
R8635:8638 SF_reduction <> k_op def
R8594:8615 Lambda.Eta <> beta_eta_eq_transitive thm
R8626:8628 LamSF_Terms <> App constr
R8650:8652 LamSF_Terms <> App constr
R8660:8662 LamSF_Terms <> Ref constr
R8654:8657 SF_reduction <> k_op def
R8631:8633 LamSF_Terms <> App constr
R8641:8643 LamSF_Terms <> Ref constr
R8635:8638 SF_reduction <> k_op def
R8594:8615 Lambda.Eta <> beta_eta_eq_transitive thm
R8740:8742 LamSF_Terms <> Ref constr
R8708:8729 Lambda.Eta <> beta_eta_eq_transitive thm
R8740:8742 LamSF_Terms <> Ref constr
R8708:8729 Lambda.Eta <> beta_eta_eq_transitive thm
R8830:8831 Homomorphism <> ap def
R8834:8836 Homomorphism <> ref def
R8856:8877 Lambda.Eta <> beta_eta_eq_transitive thm
prf 8905:8918 <> homomorphism_S
R8946:8949 Coq.Init.Logic <> :type_scope:x_'->'_x not
R8950:8960 Lambda.Eta <> beta_eta_eq ind
R8975:8979 Homomorphism <> abs_S def
R8963:8963 Homomorphism <> h var
R8966:8967 LamSF_Terms <> Op constr
R8969:8971 LamSF_Terms <> Sop constr
R8932:8943 Homomorphism <> homomorphism ind
R8945:8945 Homomorphism <> h var
R9065:9067 Coq.Init.Logic <> :type_scope:x_'='_x not
R9040:9052 Lambda.Closed <> maxvar def
R9057:9058 LamSF_Terms <> Op constr
R9060:9062 LamSF_Terms <> Sop constr
R9065:9067 Coq.Init.Logic <> :type_scope:x_'='_x not
R9040:9052 Lambda.Closed <> maxvar def
R9057:9058 LamSF_Terms <> Op constr
R9060:9062 LamSF_Terms <> Sop constr
R9135:9137 Coq.Init.Logic <> :type_scope:x_'='_x not
R9104:9117 Lambda.Terms <> lift_rec def
R9134:9134 Homomorphism <> k var
R9123:9124 LamSF_Terms <> Op constr
R9126:9128 LamSF_Terms <> Sop constr
R9141:9142 LamSF_Terms <> Op constr
R9144:9146 LamSF_Terms <> Sop constr
R9135:9137 Coq.Init.Logic <> :type_scope:x_'='_x not
R9104:9117 Lambda.Terms <> lift_rec def
R9134:9134 Homomorphism <> k var
R9123:9124 LamSF_Terms <> Op constr
R9126:9128 LamSF_Terms <> Sop constr
R9141:9142 LamSF_Terms <> Op constr
R9144:9146 LamSF_Terms <> Sop constr
R9160:9181 Lambda.Closed <> lift_rec_closed thm
R9200:9207 Lambda.Eta <> beta_eta def
R9284:9285 LamSF_Terms <> Op constr
R9287:9289 LamSF_Terms <> Sop constr
R9211:9213 Homomorphism <> abs def
R9216:9218 Homomorphism <> abs def
R9221:9223 Homomorphism <> abs def
R9226:9227 Homomorphism <> ap def
R9269:9271 Homomorphism <> ref def
R9230:9231 Homomorphism <> ap def
R9260:9262 Homomorphism <> ref def
R9234:9235 Homomorphism <> ap def
R9251:9253 Homomorphism <> ref def
R9241:9242 LamSF_Terms <> Op constr
R9244:9246 LamSF_Terms <> Sop constr
R9200:9207 Lambda.Eta <> beta_eta def
R9284:9285 LamSF_Terms <> Op constr
R9287:9289 LamSF_Terms <> Sop constr
R9211:9213 Homomorphism <> abs def
R9216:9218 Homomorphism <> abs def
R9221:9223 Homomorphism <> abs def
R9226:9227 Homomorphism <> ap def
R9269:9271 Homomorphism <> ref def
R9230:9231 Homomorphism <> ap def
R9260:9262 Homomorphism <> ref def
R9234:9235 Homomorphism <> ap def
R9251:9253 Homomorphism <> ref def
R9241:9242 LamSF_Terms <> Op constr
R9244:9246 LamSF_Terms <> Sop constr
R9332:9334 Homomorphism <> abs def
R9337:9339 Homomorphism <> abs def
R9342:9343 Homomorphism <> ap def
R9372:9374 Homomorphism <> ref def
R9346:9347 Homomorphism <> ap def
R9363:9365 Homomorphism <> ref def
R9353:9354 LamSF_Terms <> Op constr
R9356:9358 LamSF_Terms <> Sop constr
R9302:9324 Lambda.Lambda_tactics <> succ_red constr
R9332:9334 Homomorphism <> abs def
R9337:9339 Homomorphism <> abs def
R9342:9343 Homomorphism <> ap def
R9372:9374 Homomorphism <> ref def
R9346:9347 Homomorphism <> ap def
R9363:9365 Homomorphism <> ref def
R9353:9354 LamSF_Terms <> Op constr
R9356:9358 LamSF_Terms <> Sop constr
R9302:9324 Lambda.Lambda_tactics <> succ_red constr
R9391:9399 Lambda.Eta <> beta_eta1 def
R9438:9440 Homomorphism <> abs def
R9443:9445 Homomorphism <> abs def
R9448:9450 Homomorphism <> abs def
R9453:9454 Homomorphism <> ap def
R9496:9498 Homomorphism <> ref def
R9457:9458 Homomorphism <> ap def
R9487:9489 Homomorphism <> ref def
R9461:9462 Homomorphism <> ap def
R9478:9480 Homomorphism <> ref def
R9468:9469 LamSF_Terms <> Op constr
R9471:9473 LamSF_Terms <> Sop constr
R9409:9430 Lambda.Lambda_tactics <> seq_red constr
R9438:9440 Homomorphism <> abs def
R9443:9445 Homomorphism <> abs def
R9448:9450 Homomorphism <> abs def
R9453:9454 Homomorphism <> ap def
R9496:9498 Homomorphism <> ref def
R9457:9458 Homomorphism <> ap def
R9487:9489 Homomorphism <> ref def
R9461:9462 Homomorphism <> ap def
R9478:9480 Homomorphism <> ref def
R9468:9469 LamSF_Terms <> Op constr
R9471:9473 LamSF_Terms <> Sop constr
R9409:9430 Lambda.Lambda_tactics <> seq_red constr
R9522:9524 Homomorphism <> abs def
R9527:9528 Homomorphism <> ap def
R9546:9555 Lambda.Eta <> abs_etared constr
R9566:9575 Lambda.Eta <> abs_etared constr
R9588:9596 Lambda.Terms <> App constr
R9632:9634 Homomorphism <> ref def
R9599:9607 Lambda.Terms <> App constr
R9623:9625 Homomorphism <> ref def
R9613:9614 LamSF_Terms <> Op constr
R9616:9618 LamSF_Terms <> Sop constr
R9646:9659 Lambda.Terms <> lift_rec def
R9662:9663 Homomorphism <> ap def
R9692:9694 Homomorphism <> ref def
R9666:9667 Homomorphism <> ap def
R9683:9685 Homomorphism <> ref def
R9673:9674 LamSF_Terms <> Op constr
R9676:9678 LamSF_Terms <> Sop constr
R9588:9596 Lambda.Terms <> App constr
R9632:9634 Homomorphism <> ref def
R9599:9607 Lambda.Terms <> App constr
R9623:9625 Homomorphism <> ref def
R9613:9614 LamSF_Terms <> Op constr
R9616:9618 LamSF_Terms <> Sop constr
R9646:9659 Lambda.Terms <> lift_rec def
R9662:9663 Homomorphism <> ap def
R9692:9694 Homomorphism <> ref def
R9666:9667 Homomorphism <> ap def
R9683:9685 Homomorphism <> ref def
R9673:9674 LamSF_Terms <> Op constr
R9676:9678 LamSF_Terms <> Sop constr
R9714:9720 Lambda.Eta <> eta_red constr
R9734:9736 Homomorphism <> abs def
R9739:9740 Homomorphism <> ap def
R9842:9844 Homomorphism <> abs def
R9847:9848 Homomorphism <> ap def
R9864:9866 Homomorphism <> ref def
R9854:9855 LamSF_Terms <> Op constr
R9857:9859 LamSF_Terms <> Sop constr
R9812:9834 Lambda.Lambda_tactics <> succ_red constr
R9842:9844 Homomorphism <> abs def
R9847:9848 Homomorphism <> ap def
R9864:9866 Homomorphism <> ref def
R9854:9855 LamSF_Terms <> Op constr
R9857:9859 LamSF_Terms <> Sop constr
R9812:9834 Lambda.Lambda_tactics <> succ_red constr
R9882:9890 Lambda.Eta <> beta_eta1 def
R9929:9931 Homomorphism <> abs def
R9934:9936 Homomorphism <> abs def
R9939:9940 Homomorphism <> ap def
R9969:9971 Homomorphism <> ref def
R9943:9944 Homomorphism <> ap def
R9960:9962 Homomorphism <> ref def
R9950:9951 LamSF_Terms <> Op constr
R9953:9955 LamSF_Terms <> Sop constr
R9900:9921 Lambda.Lambda_tactics <> seq_red constr
R9929:9931 Homomorphism <> abs def
R9934:9936 Homomorphism <> abs def
R9939:9940 Homomorphism <> ap def
R9969:9971 Homomorphism <> ref def
R9943:9944 Homomorphism <> ap def
R9960:9962 Homomorphism <> ref def
R9950:9951 LamSF_Terms <> Op constr
R9953:9955 LamSF_Terms <> Sop constr
R9900:9921 Lambda.Lambda_tactics <> seq_red constr
R9994:9996 Homomorphism <> abs def
R9999:10000 Homomorphism <> ap def
R10018:10027 Lambda.Eta <> abs_etared constr
R10040:10048 Lambda.Terms <> App constr
R10063:10065 Homomorphism <> ref def
R10054:10055 LamSF_Terms <> Op constr
R10057:10059 LamSF_Terms <> Sop constr
R10077:10090 Lambda.Terms <> lift_rec def
R10093:10094 Homomorphism <> ap def
R10110:10112 Homomorphism <> ref def
R10100:10101 LamSF_Terms <> Op constr
R10103:10105 LamSF_Terms <> Sop constr
R10040:10048 Lambda.Terms <> App constr
R10063:10065 Homomorphism <> ref def
R10054:10055 LamSF_Terms <> Op constr
R10057:10059 LamSF_Terms <> Sop constr
R10077:10090 Lambda.Terms <> lift_rec def
R10093:10094 Homomorphism <> ap def
R10110:10112 Homomorphism <> ref def
R10100:10101 LamSF_Terms <> Op constr
R10103:10105 LamSF_Terms <> Sop constr
R10132:10138 Lambda.Eta <> eta_red constr
R10152:10154 Homomorphism <> abs def
R10157:10158 Homomorphism <> ap def
R10286:10288 Homomorphism <> abs def
R10291:10292 Homomorphism <> ap def
R10308:10310 Homomorphism <> ref def
R10298:10299 LamSF_Terms <> Op constr
R10301:10303 LamSF_Terms <> Sop constr
R10256:10277 Lambda.Lambda_tactics <> seq_red constr
R10286:10288 Homomorphism <> abs def
R10291:10292 Homomorphism <> ap def
R10308:10310 Homomorphism <> ref def
R10298:10299 LamSF_Terms <> Op constr
R10301:10303 LamSF_Terms <> Sop constr
R10256:10277 Lambda.Lambda_tactics <> seq_red constr
R10332:10334 Homomorphism <> abs def
R10337:10338 Homomorphism <> ap def
R10407:10414 Lambda.Eta <> beta_eta def
R10505:10507 Homomorphism <> abs def
R10510:10512 Homomorphism <> abs def
R10515:10517 Homomorphism <> abs def
R10523:10525 LamSF_Terms <> App constr
R10565:10567 LamSF_Terms <> Ref constr
R10528:10530 LamSF_Terms <> App constr
R10556:10558 LamSF_Terms <> Ref constr
R10533:10535 LamSF_Terms <> App constr
R10547:10549 LamSF_Terms <> Ref constr
R10538:10539 LamSF_Terms <> Op constr
R10541:10543 LamSF_Terms <> Sop constr
R10426:10428 Homomorphism <> abs def
R10431:10433 Homomorphism <> abs def