Compounds.glob

DIGEST 441145c29e73791cdc94b7f160af0742
FCompounds
R2136:2140 Coq.Arith.Arith <> <> lib
R2158:2161 Test <> <> lib
R2180:2186 General <> <> lib
R2204:2214 LamSF_Terms <> <> lib
R2233:2245 LamSF_Tactics <> <> lib
R2263:2285 LamSF_Substitution_term <> <> lib
R2304:2313 Components <> <> lib
ind 2618:2627 <> status_val
constr 2635:2643 <> Reducible
constr 2660:2662 <> Lam
constr 2717:2722 <> Active
constr 2774:2783 <> Ternary_op
constr 2799:2808 <> Binary_op0
constr 2821:2830 <> Binary_op2
constr 2843:2852 <> Binary_op1
constr 2868:2878 <> Ternary_op1
constr 2906:2913 <> Unary_op
constr 2927:2931 <> Lazy2
constr 2956:2960 <> Lazy1
constr 2984:2989 <> Eager2
constr 3008:3012 <> Eager
R2647:2656 Compounds <> status_val ind
R2673:2682 Compounds <> status_val ind
R2666:2668 Coq.Init.Datatypes <> nat ind
R2733:2742 Compounds <> status_val ind
R2726:2728 Coq.Init.Datatypes <> nat ind
R2784:2784 Compounds <> status_val ind
R2809:2809 Compounds <> status_val ind
R2831:2831 Compounds <> status_val ind
R2853:2853 Compounds <> status_val ind
R2879:2879 Compounds <> status_val ind
R2914:2914 Compounds <> status_val ind
R2932:2932 Compounds <> status_val ind
R2961:2961 Compounds <> status_val ind
R2990:2990 Compounds <> status_val ind
R3013:3013 Compounds <> status_val ind
def 3175:3180 <> status
R3186:3190 LamSF_Terms <> lamSF ind
R3203:3203 Compounds <> M var
R3213:3215 LamSF_Terms <> Ref constr
R3222:3227 Compounds <> Active constr
R3233:3234 LamSF_Terms <> Op constr
R3236:3238 LamSF_Terms <> Sop constr
R3242:3243 LamSF_Terms <> Op constr
R3245:3247 LamSF_Terms <> Aop constr
R3252:3261 Compounds <> Ternary_op constr
R3252:3261 Compounds <> Ternary_op constr
R3265:3266 LamSF_Terms <> Op constr
R3268:3270 LamSF_Terms <> Kop constr
R3275:3284 Compounds <> Binary_op0 constr
R3288:3289 LamSF_Terms <> Op constr
R3291:3293 LamSF_Terms <> Eop constr
R3298:3307 Compounds <> Binary_op2 constr
R3311:3312 LamSF_Terms <> Op constr
R3314:3316 LamSF_Terms <> Gop constr
R3320:3321 LamSF_Terms <> Op constr
R3323:3325 LamSF_Terms <> Uop constr
R3330:3339 Compounds <> Binary_op1 constr
R3330:3339 Compounds <> Binary_op1 constr
R3343:3344 LamSF_Terms <> Op constr
R3346:3348 LamSF_Terms <> Yop constr
R3353:3360 Compounds <> Unary_op constr
R3364:3365 LamSF_Terms <> Op constr
R3372:3382 Compounds <> Ternary_op1 constr
R3387:3389 LamSF_Terms <> Abs constr
R3403:3408 Compounds <> status def
R3435:3443 Compounds <> Reducible constr
R3448:3456 Compounds <> Reducible constr
R3475:3477 Compounds <> Lam constr
R3484:3488 Compounds <> Lazy1 constr
R3506:3508 Compounds <> Lam constr
R3511:3511 Coq.Init.Datatypes <> S constr
R3519:3521 Compounds <> Lam constr
R3542:3547 Compounds <> Active constr
R3554:3558 Compounds <> Lazy1 constr
R3576:3581 Compounds <> Active constr
R3584:3584 Coq.Init.Datatypes <> S constr
R3592:3594 Compounds <> Lam constr
R3620:3624 Compounds <> Lazy1 constr
R3645:3647 LamSF_Terms <> App constr
R3664:3669 Compounds <> status def
R3696:3704 Compounds <> Reducible constr
R3709:3717 Compounds <> Reducible constr
R3736:3738 Compounds <> Lam constr
R3745:3753 Compounds <> Reducible constr
R3771:3776 Compounds <> Active constr
R3783:3788 Compounds <> Active constr
R3844:3853 Compounds <> Ternary_op constr
R3858:3862 Compounds <> Lazy2 constr
R3881:3890 Compounds <> Binary_op0 constr
R3895:3899 Compounds <> Lazy1 constr
R3918:3927 Compounds <> Binary_op2 constr
R3955:3960 Compounds <> status def
R3991:3999 Compounds <> Reducible constr
R4004:4012 Compounds <> Reducible constr
R4035:4037 Compounds <> Lam constr
R4044:4049 Compounds <> Active constr
R4074:4079 Compounds <> Active constr
R4086:4091 Compounds <> Active constr
R4116:4125 Compounds <> Ternary_op constr
R4148:4157 Compounds <> Binary_op0 constr
R4179:4188 Compounds <> Binary_op2 constr
R4211:4220 Compounds <> Binary_op1 constr
R4243:4253 Compounds <> Ternary_op1 constr
R4276:4283 Compounds <> Unary_op constr
R4288:4292 Compounds <> Eager constr
R4288:4292 Compounds <> Eager constr
R4288:4292 Compounds <> Eager constr
R4288:4292 Compounds <> Eager constr
R4288:4292 Compounds <> Eager constr
R4288:4292 Compounds <> Eager constr
R4319:4327 Compounds <> Reducible constr
R4366:4375 Compounds <> Binary_op1 constr
R4380:4384 Compounds <> Eager constr
R4403:4413 Compounds <> Ternary_op1 constr
R4418:4423 Compounds <> Eager2 constr
R4441:4448 Compounds <> Unary_op constr
R4453:4461 Compounds <> Reducible constr
R4479:4483 Compounds <> Lazy2 constr
R4488:4492 Compounds <> Lazy1 constr
R4511:4515 Compounds <> Lazy1 constr
R4520:4528 Compounds <> Reducible constr
R4547:4552 Compounds <> Eager2 constr
R4557:4561 Compounds <> Eager constr
R4580:4584 Compounds <> Eager constr
R4612:4617 Compounds <> status def
R4648:4650 Compounds <> Lam constr
R4657:4662 Compounds <> Active constr
R4687:4692 Compounds <> Active constr
R4699:4704 Compounds <> Active constr
R4734:4742 Compounds <> Reducible constr
prf 4796:4808 <> star_compound
R4846:4849 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4838:4840 Coq.Init.Logic <> :type_scope:x_'='_x not
R4823:4828 Compounds <> status def
R4831:4834 Components <> star def
R4836:4836 Compounds <> M var
R4841:4845 Compounds <> Lazy1 constr
R4864:4866 Coq.Init.Logic <> :type_scope:x_'='_x not
R4850:4855 Compounds <> status def
R4857:4860 Components <> star def
R4862:4862 Compounds <> M var
R4867:4871 Compounds <> Lazy2 constr
def 4950:4957 <> compound
R4965:4965 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4982:4987 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4974:4976 Coq.Init.Logic <> :type_scope:x_'='_x not
R4966:4971 Compounds <> status def
R4973:4973 Compounds <> M var
R4977:4981 Compounds <> Lazy2 constr
R4988:4988 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5005:5010 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R4997:4999 Coq.Init.Logic <> :type_scope:x_'='_x not
R4989:4994 Compounds <> status def
R4996:4996 Compounds <> M var
R5000:5004 Compounds <> Lazy1 constr
R5011:5011 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5029:5035 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5052:5052 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5020:5022 Coq.Init.Logic <> :type_scope:x_'='_x not
R5012:5017 Compounds <> status def
R5019:5019 Compounds <> M var
R5023:5028 Compounds <> Eager2 constr
R5044:5046 Coq.Init.Logic <> :type_scope:x_'='_x not
R5036:5041 Compounds <> status def
R5043:5043 Compounds <> M var
R5047:5051 Compounds <> Eager constr
def 5068:5077 <> factorable
R5085:5085 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5107:5111 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5094:5096 Coq.Init.Logic <> :type_scope:x_'='_x not
R5086:5091 Compounds <> status def
R5093:5093 Compounds <> M var
R5097:5106 Compounds <> Ternary_op constr
R5112:5112 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5134:5138 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5121:5123 Coq.Init.Logic <> :type_scope:x_'='_x not
R5113:5118 Compounds <> status def
R5120:5120 Compounds <> M var
R5124:5133 Compounds <> Binary_op0 constr
R5139:5139 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5161:5166 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5148:5150 Coq.Init.Logic <> :type_scope:x_'='_x not
R5140:5145 Compounds <> status def
R5147:5147 Compounds <> M var
R5151:5160 Compounds <> Binary_op2 constr
R5167:5167 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5189:5194 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5176:5178 Coq.Init.Logic <> :type_scope:x_'='_x not
R5168:5173 Compounds <> status def
R5175:5175 Compounds <> M var
R5179:5188 Compounds <> Binary_op1 constr
R5195:5195 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5218:5222 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5204:5206 Coq.Init.Logic <> :type_scope:x_'='_x not
R5196:5201 Compounds <> status def
R5203:5203 Compounds <> M var
R5207:5217 Compounds <> Ternary_op1 constr
R5223:5223 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5243:5247 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5232:5234 Coq.Init.Logic <> :type_scope:x_'='_x not
R5224:5229 Compounds <> status def
R5231:5231 Compounds <> M var
R5235:5242 Compounds <> Unary_op constr
R5248:5248 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5265:5270 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5257:5259 Coq.Init.Logic <> :type_scope:x_'='_x not
R5249:5254 Compounds <> status def
R5256:5256 Compounds <> M var
R5260:5264 Compounds <> Lazy2 constr
R5271:5271 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5288:5293 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5280:5282 Coq.Init.Logic <> :type_scope:x_'='_x not
R5272:5277 Compounds <> status def
R5279:5279 Compounds <> M var
R5283:5287 Compounds <> Lazy1 constr
R5294:5294 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5312:5318 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5335:5335 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R5303:5305 Coq.Init.Logic <> :type_scope:x_'='_x not
R5295:5300 Compounds <> status def
R5302:5302 Compounds <> M var
R5306:5311 Compounds <> Eager2 constr
R5327:5329 Coq.Init.Logic <> :type_scope:x_'='_x not
R5319:5324 Compounds <> status def
R5326:5326 Compounds <> M var
R5330:5334 Compounds <> Eager constr
prf 5346:5369 <> compounds_are_factorable
R5396:5405 Compounds <> factorable def
R5407:5407 Compounds <> M var
R5382:5389 Compounds <> compound def
R5391:5391 Compounds <> M var
R5436:5445 Compounds <> factorable def
prf 5495:5531 <> factorable_applications_are_compounds
R5571:5578 Compounds <> compound def
R5580:5582 LamSF_Terms <> App constr
R5586:5586 Compounds <> N var
R5584:5584 Compounds <> M var
R5547:5556 Compounds <> factorable def
R5559:5561 LamSF_Terms <> App constr
R5565:5565 Compounds <> N var
R5563:5563 Compounds <> M var
R5604:5613 Compounds <> factorable def
R5616:5623 Compounds <> compound def
R5649:5654 Compounds <> status def
R5649:5654 Compounds <> status def
R5894:5899 Compounds <> status def
R5894:5899 Compounds <> status def
R6136:6141 Compounds <> status def
R6136:6141 Compounds <> status def
prf 6370:6406 <> factorable_abstractions_are_compounds
R6442:6449 Compounds <> compound def
R6452:6454 LamSF_Terms <> Abs constr
R6456:6456 Compounds <> M var
R6420:6429 Compounds <> factorable def
R6432:6434 LamSF_Terms <> Abs constr
R6436:6436 Compounds <> M var
R6475:6484 Compounds <> factorable def
R6487:6494 Compounds <> compound def
R6520:6525 Compounds <> status def
R6520:6525 Compounds <> status def
prf 6577:6615 <> factorable_implies_compound_or_operator
R6656:6659 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R6646:6653 Compounds <> compound def
R6655:6655 Compounds <> M var
R6660:6666 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6668:6669 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R6671:6673 Coq.Init.Logic <> :type_scope:x_'='_x not
R6670:6670 Compounds <> M var
R6674:6675 LamSF_Terms <> Op constr
R6677:6677 Compounds <> o var
R6629:6638 Compounds <> factorable def
R6640:6640 Compounds <> M var
R6696:6705 Compounds <> factorable def
R6708:6715 Compounds <> compound def
R6779:6784 Compounds <> status def
R6779:6784 Compounds <> status def
R6833:6838 Compounds <> status def
R6864:6869 Compounds <> status def
R6833:6838 Compounds <> status def
R6864:6869 Compounds <> status def
R6864:6869 Compounds <> status def
def 6905:6926 <> preserves_components_l
R6934:6940 LamSF_Tactics <> termred def
R7006:7010 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R6994:7003 Compounds <> factorable def
R7005:7005 Compounds <> N var
R7011:7020 LamSF_Tactics <> multi_step ind
R7046:7059 Components <> left_component def
R7061:7061 Compounds <> N var
R7027:7040 Components <> left_component def
R7042:7042 Compounds <> M var
R7022:7024 Compounds <> red var
R6983:6985 Compounds <> red var
R6989:6989 Compounds <> N var
R6987:6987 Compounds <> M var
R6957:6966 Compounds <> factorable def
R6968:6968 Compounds <> M var
prf 7072:7104 <> preserves_components_l_multi_step
R7222:7226 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R7210:7219 Compounds <> factorable def
R7221:7221 Compounds <> N var
R7227:7236 LamSF_Tactics <> multi_step ind
R7262:7275 Components <> left_component def
R7277:7277 Compounds <> N var
R7243:7256 Components <> left_component def
R7258:7258 Compounds <> M var
R7238:7240 Compounds <> red var
R7188:7197 LamSF_Tactics <> multi_step ind
R7205:7205 Compounds <> N var
R7203:7203 Compounds <> M var
R7199:7201 Compounds <> red var
R7162:7171 Compounds <> factorable def
R7173:7173 Compounds <> M var
R7121:7142 Compounds <> preserves_components_l def
R7144:7146 Compounds <> red var
R7388:7401 Components <> left_component def
R7367:7380 LamSF_Tactics <> transitive_red thm
R7388:7401 Components <> left_component def
R7367:7380 LamSF_Tactics <> transitive_red thm
def 7475:7496 <> preserves_components_r
R7504:7510 LamSF_Tactics <> termred def
R7576:7580 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R7564:7573 Compounds <> factorable def
R7575:7575 Compounds <> N var
R7581:7590 LamSF_Tactics <> multi_step ind
R7617:7631 Components <> right_component def
R7633:7633 Compounds <> N var
R7597:7611 Components <> right_component def
R7613:7613 Compounds <> M var
R7592:7594 Compounds <> red var
R7553:7555 Compounds <> red var
R7559:7559 Compounds <> N var
R7557:7557 Compounds <> M var
R7527:7536 Compounds <> factorable def
R7538:7538 Compounds <> M var
prf 7644:7676 <> preserves_components_r_multi_step
R7794:7798 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R7782:7791 Compounds <> factorable def
R7793:7793 Compounds <> N var
R7799:7808 LamSF_Tactics <> multi_step ind
R7835:7849 Components <> right_component def
R7851:7851 Compounds <> N var
R7815:7829 Components <> right_component def
R7831:7831 Compounds <> M var
R7810:7812 Compounds <> red var
R7760:7769 LamSF_Tactics <> multi_step ind
R7777:7777 Compounds <> N var
R7775:7775 Compounds <> M var
R7771:7773 Compounds <> red var
R7734:7743 Compounds <> factorable def
R7745:7745 Compounds <> M var
R7693:7714 Compounds <> preserves_components_r def
R7716:7718 Compounds <> red var
R7962:7976 Components <> right_component def
R7941:7954 LamSF_Tactics <> transitive_red thm
R7962:7976 Components <> right_component def
R7941:7954 LamSF_Tactics <> transitive_red thm
def 8049:8063 <> relocate_status
R8081:8081 Compounds <> a var
R8091:8093 Compounds <> Lam constr
R8100:8102 Compounds <> Lam constr
R8105:8112 LamSF_Terms <> relocate def
R8118:8118 Compounds <> k var
R8116:8116 Compounds <> n var
R8123:8128 Compounds <> Active constr
R8135:8140 Compounds <> Active constr
R8143:8150 LamSF_Terms <> relocate def
R8156:8156 Compounds <> k var
R8154:8154 Compounds <> n var
R8166:8166 Compounds <> a var
prf 8184:8198 <> rank_compound_l
R8249:8251 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8226:8229 Components <> rank def
R8232:8245 Components <> left_component def
R8247:8247 Compounds <> M var
R8252:8255 Components <> rank def
R8257:8257 Compounds <> M var
R8212:8219 Compounds <> compound def
R8221:8221 Compounds <> M var
R8298:8305 Compounds <> compound def
R8298:8305 Compounds <> compound def
R8298:8305 Compounds <> compound def
R8298:8305 Compounds <> compound def
R8391:8392 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8385:8388 Components <> rank def
R8406:8418 Components <> rank_positive thm
R8391:8392 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8385:8388 Components <> rank def
R8406:8418 Components <> rank_positive thm
R8451:8452 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8445:8448 Components <> rank def
R8466:8478 Components <> rank_positive thm
R8451:8452 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R8445:8448 Components <> rank def
R8466:8478 Components <> rank_positive thm
R8517:8522 Compounds <> status def
R8517:8522 Compounds <> status def
R8565:8570 Compounds <> status def
R8565:8570 Compounds <> status def
prf 8598:8612 <> rank_compound_r
R8664:8666 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8640:8643 Components <> rank def
R8646:8660 Components <> right_component def
R8662:8662 Compounds <> M var
R8667:8670 Components <> rank def
R8672:8672 Compounds <> M var
R8626:8633 Compounds <> compound def
R8635:8635 Compounds <> M var
R8713:8720 Compounds <> compound def
R8713:8720 Compounds <> compound def
R8713:8720 Compounds <> compound def
R8713:8720 Compounds <> compound def
R8805:8810 Compounds <> status def
R8805:8810 Compounds <> status def
R8859:8864 Compounds <> status def
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8859:8864 Compounds <> status def
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8891:8893 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R8878:8881 Components <> rank def
R8884:8887 Components <> star def
R8894:8897 Components <> rank def
R8900:8902 LamSF_Terms <> Abs constr
R8919:8927 Components <> rank_star thm
R8978:8983 Compounds <> status def
R8978:8983 Compounds <> status def
R9017:9022 Compounds <> status def
R9017:9022 Compounds <> status def
R9049:9054 Compounds <> status def
R9049:9054 Compounds <> status def
prf 9083:9107 <> lift_rec_preserves_status
R9123:9127 LamSF_Terms <> lamSF ind
R9136:9138 Coq.Init.Datatypes <> nat ind
R9165:9167 Coq.Init.Logic <> :type_scope:x_'='_x not
R9142:9147 Compounds <> status def
R9150:9157 LamSF_Terms <> lift_rec def
R9163:9163 Compounds <> k var
R9161:9161 Compounds <> n var
R9159:9159 Compounds <> M var
R9168:9182 Compounds <> relocate_status def
R9197:9197 Compounds <> k var
R9195:9195 Compounds <> n var
R9185:9190 Compounds <> status def
R9192:9192 Compounds <> M var
R9257:9269 LamSF_Tactics <> relocate_succ thm
R9257:9269 LamSF_Tactics <> relocate_succ thm
R9257:9269 LamSF_Tactics <> relocate_succ thm
R9257:9269 LamSF_Tactics <> relocate_succ thm
R9371:9385 Compounds <> relocate_status def
R9395:9400 Compounds <> status def
R9395:9400 Compounds <> status def
R9425:9432 LamSF_Terms <> relocate def
R9441:9444 Test <> test def
R9447:9447 Coq.Init.Datatypes <> S constr
R9441:9444 Test <> test def
R9447:9447 Coq.Init.Datatypes <> S constr
R9490:9491 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9502:9502 Coq.Init.Datatypes <> S constr
R9506:9506 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9507:9510 Coq.Init.Peano <> pred def
R9502:9502 Coq.Init.Datatypes <> S constr
R9506:9506 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9507:9510 Coq.Init.Peano <> pred def
R9490:9491 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9545:9545 Coq.Init.Datatypes <> S constr
R9548:9551 Coq.Init.Peano <> pred def
R9545:9545 Coq.Init.Datatypes <> S constr
R9548:9551 Coq.Init.Peano <> pred def
R9574:9577 Test <> test def
R9582:9585 Coq.Init.Peano <> pred def
R9574:9577 Test <> test def
R9582:9585 Coq.Init.Peano <> pred def
R9637:9640 Test <> test def
R9637:9640 Test <> test def
R9679:9686 LamSF_Terms <> relocate def
R9695:9698 Test <> test def
R9701:9701 Coq.Init.Datatypes <> S constr
R9695:9698 Test <> test def
R9701:9701 Coq.Init.Datatypes <> S constr
R9744:9745 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9756:9756 Coq.Init.Datatypes <> S constr
R9760:9760 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9761:9764 Coq.Init.Peano <> pred def
R9756:9756 Coq.Init.Datatypes <> S constr
R9760:9760 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9761:9764 Coq.Init.Peano <> pred def
R9744:9745 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R9799:9799 Coq.Init.Datatypes <> S constr
R9802:9805 Coq.Init.Peano <> pred def
R9799:9799 Coq.Init.Datatypes <> S constr
R9802:9805 Coq.Init.Peano <> pred def
R9828:9831 Test <> test def
R9836:9839 Coq.Init.Peano <> pred def
R9828:9831 Test <> test def
R9836:9839 Coq.Init.Peano <> pred def
R9891:9894 Test <> test def
R9891:9894 Test <> test def
R9968:9982 Compounds <> relocate_status def
R9992:9997 Compounds <> status def
R10047:10061 Compounds <> relocate_status def
R10070:10075 Compounds <> status def
R9992:9997 Compounds <> status def
R10070:10075 Compounds <> status def
R10070:10075 Compounds <> status def
R10115:10139 Compounds <> lift_rec_preserves_status thm
prf 10150:10159 <> lam_is_abs
R10195:10201 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10203:10204 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R10206:10208 Coq.Init.Logic <> :type_scope:x_'='_x not
R10205:10205 Compounds <> M var
R10209:10211 LamSF_Terms <> Abs constr
R10213:10213 Compounds <> N var
R10183:10185 Coq.Init.Logic <> :type_scope:x_'='_x not
R10175:10180 Compounds <> status def
R10182:10182 Compounds <> M var
R10186:10188 Compounds <> Lam constr
R10190:10190 Compounds <> i var
R10284:10289 Compounds <> status def
R10308:10313 Compounds <> status def
R10284:10289 Compounds <> status def
R10308:10313 Compounds <> status def
R10308:10313 Compounds <> status def
prf 10336:10361 <> subst_rec_preserves_status
R10376:10380 LamSF_Terms <> lamSF ind
R10387:10389 Coq.Init.Datatypes <> nat ind
R10515:10517 Coq.Init.Logic <> :type_scope:x_'='_x not
R10491:10496 Compounds <> status def
R10499:10507 LamSF_Terms <> subst_rec def
R10513:10513 Compounds <> k var
R10511:10511 Compounds <> N var
R10509:10509 Compounds <> M var
R10518:10523 Compounds <> status def
R10525:10525 Compounds <> M var
R10471:10473 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10470:10470 Compounds <> i var
R10474:10474 Compounds <> k var
R10458:10460 Coq.Init.Logic <> :type_scope:x_'='_x not
R10450:10455 Compounds <> status def
R10457:10457 Compounds <> M var
R10461:10463 Compounds <> Lam constr
R10465:10465 Compounds <> i var
R10429:10431 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10428:10428 Compounds <> i var
R10432:10432 Compounds <> k var
R10413:10415 Coq.Init.Logic <> :type_scope:x_'='_x not
R10405:10410 Compounds <> status def
R10412:10412 Compounds <> M var
R10416:10421 Compounds <> Active constr
R10423:10423 Compounds <> i var
R10678:10683 Compounds <> status def
R10678:10683 Compounds <> status def
R10866:10866 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R10866:10866 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11032:11032 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11032:11032 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11130:11136 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11138:11139 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11142:11144 Coq.Init.Logic <> :type_scope:x_'='_x not
R11145:11147 LamSF_Terms <> Abs constr
R11149:11149 Compounds <> N var
R11118:11120 Coq.Init.Logic <> :type_scope:x_'='_x not
R11109:11114 Compounds <> status def
R11121:11123 Compounds <> Lam constr
R11125:11125 Compounds <> i var
R11130:11136 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11138:11139 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11142:11144 Coq.Init.Logic <> :type_scope:x_'='_x not
R11145:11147 LamSF_Terms <> Abs constr
R11149:11149 Compounds <> N var
R11118:11120 Coq.Init.Logic <> :type_scope:x_'='_x not
R11109:11114 Compounds <> status def
R11121:11123 Compounds <> Lam constr
R11125:11125 Compounds <> i var
R11163:11172 Compounds <> lam_is_abs thm
R11210:11215 Compounds <> status def
R11210:11215 Compounds <> status def
R11290:11296 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11298:11299 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11302:11304 Coq.Init.Logic <> :type_scope:x_'='_x not
R11305:11307 LamSF_Terms <> Abs constr
R11309:11309 Compounds <> N var
R11290:11296 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11298:11299 Coq.Init.Logic <> :type_scope:'exists'_x_'..'_x_','_x not
R11302:11304 Coq.Init.Logic <> :type_scope:x_'='_x not
R11305:11307 LamSF_Terms <> Abs constr
R11309:11309 Compounds <> N var
R11358:11363 Compounds <> status def
R11366:11374 LamSF_Terms <> subst_rec def
R11381:11381 Coq.Init.Datatypes <> S constr
R11358:11363 Compounds <> status def
R11366:11374 LamSF_Terms <> subst_rec def
R11381:11381 Coq.Init.Datatypes <> S constr
prf 11772:11791 <> rank_component_app_l
R11838:11840 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11807:11810 Components <> rank def
R11813:11826 Components <> left_component def
R11829:11831 LamSF_Terms <> App constr
R11835:11835 Compounds <> N var
R11833:11833 Compounds <> M var
R11841:11844 Components <> rank def
R11847:11849 LamSF_Terms <> App constr
R11853:11853 Compounds <> N var
R11851:11851 Compounds <> M var
prf 11896:11915 <> rank_component_app_r
R11963:11965 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R11931:11934 Components <> rank def
R11937:11951 Components <> right_component def
R11954:11956 LamSF_Terms <> App constr
R11960:11960 Compounds <> N var
R11958:11958 Compounds <> M var
R11966:11969 Components <> rank def
R11972:11974 LamSF_Terms <> App constr
R11978:11978 Compounds <> N var
R11976:11976 Compounds <> M var
prf 12021:12040 <> rank_component_abs_l
R12083:12085 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R12054:12057 Components <> rank def
R12060:12073 Components <> left_component def
R12076:12078 LamSF_Terms <> Abs constr
R12080:12080 Compounds <> M var
R12086:12089 Components <> rank def
R12092:12094 LamSF_Terms <> Abs constr
R12096:12096 Compounds <> M var
R12217:12218 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R12211:12214 Components <> rank def
R12217:12218 Coq.Init.Peano <> :nat_scope:x_'>'_x not
R12211:12214 Components <> rank def
R12233:12245 Components <> rank_positive thm
R12256:12269 Components <> left_component def
R12290:12293 Components <> rank def
R12301:12304 Components <> rank def
R12301:12304 Components <> rank def
R12325:12328 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12346:12346 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12317:12324 Components <> abs_rank def
R12337:12339 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12329:12336 Components <> abs_rank def
R12340:12343 Components <> rank def
R12374:12376 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12363:12365 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12355:12362 Components <> abs_rank def
R12366:12373 Components <> abs_rank def
R12377:12380 Components <> rank def
R12374:12376 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12363:12365 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12355:12362 Components <> abs_rank def
R12366:12373 Components <> abs_rank def
R12377:12380 Components <> rank def
R12325:12328 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12346:12346 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12317:12324 Components <> abs_rank def
R12337:12339 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12329:12336 Components <> abs_rank def
R12340:12343 Components <> rank def
R12464:12467 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R12399:12399 Coq.Init.Datatypes <> S constr
R12435:12437 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12402:12402 Coq.Init.Datatypes <> S constr
R12406:12408 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12409:12409 Coq.Init.Datatypes <> S constr
R12429:12431 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12412:12412 Coq.Init.Datatypes <> S constr
R12416:12418 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12419:12419 Coq.Init.Datatypes <> S constr
R12423:12425 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12438:12438 Coq.Init.Datatypes <> S constr
R12442:12444 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12445:12445 Coq.Init.Datatypes <> S constr
R12457:12459 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12448:12448 Coq.Init.Datatypes <> S constr
R12452:12454 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12476:12478 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12468:12475 Components <> abs_rank def
R12479:12486 Components <> abs_rank def
R12464:12467 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R12399:12399 Coq.Init.Datatypes <> S constr
R12435:12437 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12402:12402 Coq.Init.Datatypes <> S constr
R12406:12408 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12409:12409 Coq.Init.Datatypes <> S constr
R12429:12431 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12412:12412 Coq.Init.Datatypes <> S constr
R12416:12418 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12419:12419 Coq.Init.Datatypes <> S constr
R12423:12425 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12438:12438 Coq.Init.Datatypes <> S constr
R12442:12444 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12445:12445 Coq.Init.Datatypes <> S constr
R12457:12459 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12448:12448 Coq.Init.Datatypes <> S constr
R12452:12454 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12476:12478 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12468:12475 Components <> abs_rank def
R12479:12486 Components <> abs_rank def
R12501:12508 Components <> abs_rank def
R12546:12549 Components <> rank def
R12561:12563 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12577:12577 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12564:12567 Coq.Init.Peano <> pred def
R12570:12573 Components <> rank def
R12561:12563 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12577:12577 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12564:12567 Coq.Init.Peano <> pred def
R12570:12573 Components <> rank def
R12546:12549 Components <> rank def
R12618:12621 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12640:12640 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12607:12609 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12599:12606 Components <> abs_rank def
R12610:12617 Components <> abs_rank def
R12623:12625 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12639:12639 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12626:12629 Coq.Init.Peano <> pred def
R12632:12635 Components <> rank def
R12668:12670 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12657:12659 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12649:12656 Components <> abs_rank def
R12660:12667 Components <> abs_rank def
R12690:12693 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12707:12707 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12679:12681 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12671:12678 Components <> abs_rank def
R12682:12689 Components <> abs_rank def
R12694:12697 Coq.Init.Peano <> pred def
R12700:12703 Components <> rank def
R12668:12670 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12657:12659 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12649:12656 Components <> abs_rank def
R12660:12667 Components <> abs_rank def
R12690:12693 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12707:12707 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12679:12681 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12671:12678 Components <> abs_rank def
R12682:12689 Components <> abs_rank def
R12694:12697 Coq.Init.Peano <> pred def
R12700:12703 Components <> rank def
R12618:12621 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12640:12640 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12607:12609 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12599:12606 Components <> abs_rank def
R12610:12617 Components <> abs_rank def
R12623:12625 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12639:12639 Coq.Init.Peano <> :nat_scope:x_'+'_x not
R12626:12629 Coq.Init.Peano <> pred def
R12632:12635 Components <> rank def
R12727:12734 Components <> abs_left def
R12737:12744 Components <> abs_rank def
R12765:12768 Components <> rank def
R12785:12785 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R12787:12787 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12785:12785 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R12787:12787 Coq.Init.Peano <> :nat_scope:x_'*'_x not
R12834:12847 Components <> left_component def
R12850:12857 Components <> abs_left def
R12860:12867 Components <> abs_rank def
prf 12911:12930 <> rank_component_abs_r
R12974:12976 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R12944:12947 Components <> rank def
R12950:12964 Components <> right_component def
R12967:12969 LamSF_Terms <> Abs constr
R12971:12971 Compounds <> M var
R12977:12980 Components <> rank def
R12983:12985 LamSF_Terms <> Abs constr
R12987:12987 Compounds <> M var
R13007:13021 Components <> right_component def
R13041:13049 Components <> rank_star thm
prf 13069:13099 <> subst_rec_preserves_star_active
R13116:13120 LamSF_Terms <> lamSF ind
R13188:13190 Coq.Init.Logic <> :type_scope:x_'='_x not
R13167:13175 LamSF_Terms <> subst_rec def
R13187:13187 Compounds <> k var
R13185:13185 Compounds <> N var
R13177:13180 Components <> star def
R13182:13182 Compounds <> M var
R13191:13194 Components <> star def
R13197:13205 LamSF_Terms <> subst_rec def
R13212:13212 Coq.Init.Datatypes <> S constr
R13214:13214 Compounds <> k var
R13209:13209 Compounds <> N var
R13207:13207 Compounds <> M var
R13154:13157 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R13153:13153 Compounds <> i var
R13158:13158 Compounds <> k var
R13138:13140 Coq.Init.Logic <> :type_scope:x_'='_x not
R13130:13135 Compounds <> status def
R13137:13137 Compounds <> M var
R13141:13146 Compounds <> Active constr
R13148:13148 Compounds <> i var
R13274:13283 LamSF_Terms <> insert_Ref def
R13291:13297 Test <> compare def
R13311:13317 Test <> compare def
R13326:13326 Coq.Init.Datatypes <> S constr
R13320:13320 Coq.Init.Datatypes <> S constr
R13291:13297 Test <> compare def
R13311:13317 Test <> compare def
R13326:13326 Coq.Init.Datatypes <> S constr
R13320:13320 Coq.Init.Datatypes <> S constr
R13311:13317 Test <> compare def
R13326:13326 Coq.Init.Datatypes <> S constr
R13320:13320 Coq.Init.Datatypes <> S constr
R13511:13516 Compounds <> status def
R13511:13516 Compounds <> status def
R13532:13540 LamSF_Terms <> subst_rec def
R13554:13554 Coq.Init.Datatypes <> S constr
R13543:13546 Components <> star def
R13566:13569 Components <> star def
R13572:13580 LamSF_Terms <> subst_rec def
R13587:13587 Coq.Init.Datatypes <> S constr
R13589:13589 Coq.Init.Datatypes <> S constr
R13566:13569 Components <> star def
R13572:13580 LamSF_Terms <> subst_rec def
R13587:13587 Coq.Init.Datatypes <> S constr
R13589:13589 Coq.Init.Datatypes <> S constr
R13532:13540 LamSF_Terms <> subst_rec def
R13554:13554 Coq.Init.Datatypes <> S constr
R13543:13546 Components <> star def
R13614:13619 Coq.Init.Logic <> eq_sym thm
prf 13680:13707 <> subst_rec_preserves_star_lam
R13724:13728 LamSF_Terms <> lamSF ind
R13793:13795 Coq.Init.Logic <> :type_scope:x_'='_x not
R13772:13780 LamSF_Terms <> subst_rec def
R13792:13792 Compounds <> k var
R13790:13790 Compounds <> N var
R13782:13785 Components <> star def
R13787:13787 Compounds <> M var
R13796:13799 Components <> star def
R13802:13810 LamSF_Terms <> subst_rec def
R13817:13817 Coq.Init.Datatypes <> S constr
R13819:13819 Compounds <> k var
R13814:13814 Compounds <> N var
R13812:13812 Compounds <> M var
R13759:13762 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R13758:13758 Compounds <> i var
R13763:13763 Compounds <> k var
R13746:13748 Coq.Init.Logic <> :type_scope:x_'='_x not
R13738:13743 Compounds <> status def
R13745:13745 Compounds <> M var
R13749:13751 Compounds <> Lam constr
R13753:13753 Compounds <> i var
R13884:13887 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R13872:13874 Coq.Init.Logic <> :type_scope:x_'='_x not
R13864:13869 Compounds <> status def
R13875:13877 Compounds <> Lam constr
R13880:13880 Coq.Init.Datatypes <> S constr
R13896:13898 Coq.Init.Logic <> :type_scope:x_'='_x not
R13888:13893 Compounds <> status def
R13899:13904 Compounds <> Active constr
R13907:13907 Coq.Init.Datatypes <> S constr
R13884:13887 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R13872:13874 Coq.Init.Logic <> :type_scope:x_'='_x not
R13864:13869 Compounds <> status def
R13875:13877 Compounds <> Lam constr
R13880:13880 Coq.Init.Datatypes <> S constr
R13896:13898 Coq.Init.Logic <> :type_scope:x_'='_x not
R13888:13893 Compounds <> status def
R13899:13904 Compounds <> Active constr
R13907:13907 Coq.Init.Datatypes <> S constr
R13932:13937 Compounds <> status def
R13932:13937 Compounds <> status def
R14030:14030 Coq.Init.Datatypes <> S constr
R14024:14024 Coq.Init.Datatypes <> S constr
R14030:14030 Coq.Init.Datatypes <> S constr
R14024:14024 Coq.Init.Datatypes <> S constr
R14069:14099 Compounds <> subst_rec_preserves_star_active thm
R14112:14112 Coq.Init.Datatypes <> S constr
R14106:14106 Coq.Init.Datatypes <> S constr
R14069:14099 Compounds <> subst_rec_preserves_star_active thm
R14112:14112 Coq.Init.Datatypes <> S constr
R14106:14106 Coq.Init.Datatypes <> S constr
prf 14148:14182 <> subst_rec_preserves_star_factorable
R14199:14203 LamSF_Terms <> lamSF ind
R14251:14253 Coq.Init.Logic <> :type_scope:x_'='_x not
R14230:14238 LamSF_Terms <> subst_rec def
R14250:14250 Compounds <> k var
R14248:14248 Compounds <> N var
R14240:14243 Components <> star def
R14245:14245 Compounds <> M var
R14254:14257 Components <> star def
R14259:14267 LamSF_Terms <> subst_rec def
R14274:14274 Coq.Init.Datatypes <> S constr
R14276:14276 Compounds <> k var
R14271:14271 Compounds <> N var
R14269:14269 Compounds <> M var
R14211:14220 Compounds <> factorable def
R14222:14222 Compounds <> M var
R14318:14327 Compounds <> factorable def
R14318:14327 Compounds <> factorable def
R14391:14396 Compounds <> status def
R14391:14396 Compounds <> status def
R14882:14884 Coq.Init.Logic <> :type_scope:x_'='_x not
R14446:14451 Compounds <> status def
R14469:14477 Compounds <> Reducible constr
R14482:14490 Compounds <> Reducible constr
R14501:14503 Compounds <> Lam constr
R14510:14514 Compounds <> Lazy1 constr
R14525:14527 Compounds <> Lam constr
R14530:14530 Coq.Init.Datatypes <> S constr
R14538:14540 Compounds <> Lam constr
R14553:14558 Compounds <> Active constr
R14565:14569 Compounds <> Lazy1 constr
R14580:14585 Compounds <> Active constr
R14588:14588 Coq.Init.Datatypes <> S constr
R14596:14598 Compounds <> Lam constr
R14611:14620 Compounds <> Ternary_op constr
R14625:14629 Compounds <> Lazy1 constr
R14640:14649 Compounds <> Binary_op0 constr
R14654:14658 Compounds <> Lazy1 constr
R14669:14678 Compounds <> Binary_op2 constr
R14683:14687 Compounds <> Lazy1 constr
R14698:14707 Compounds <> Binary_op1 constr
R14712:14716 Compounds <> Lazy1 constr
R14727:14737 Compounds <> Ternary_op1 constr
R14742:14746 Compounds <> Lazy1 constr
R14757:14764 Compounds <> Unary_op constr
R14769:14773 Compounds <> Lazy1 constr
R14784:14788 Compounds <> Lazy2 constr
R14793:14797 Compounds <> Lazy1 constr
R14808:14812 Compounds <> Lazy1 constr
R14817:14821 Compounds <> Lazy1 constr
R14832:14837 Compounds <> Eager2 constr
R14842:14846 Compounds <> Lazy1 constr
R14857:14861 Compounds <> Eager constr
R14866:14870 Compounds <> Lazy1 constr
R14885:14889 Compounds <> Lazy1 constr
R14882:14884 Coq.Init.Logic <> :type_scope:x_'='_x not
R14446:14451 Compounds <> status def
R14469:14477 Compounds <> Reducible constr
R14482:14490 Compounds <> Reducible constr
R14501:14503 Compounds <> Lam constr
R14510:14514 Compounds <> Lazy1 constr
R14525:14527 Compounds <> Lam constr
R14530:14530 Coq.Init.Datatypes <> S constr
R14538:14540 Compounds <> Lam constr
R14553:14558 Compounds <> Active constr
R14565:14569 Compounds <> Lazy1 constr
R14580:14585 Compounds <> Active constr
R14588:14588 Coq.Init.Datatypes <> S constr
R14596:14598 Compounds <> Lam constr
R14611:14620 Compounds <> Ternary_op constr
R14625:14629 Compounds <> Lazy1 constr
R14640:14649 Compounds <> Binary_op0 constr
R14654:14658 Compounds <> Lazy1 constr
R14669:14678 Compounds <> Binary_op2 constr
R14683:14687 Compounds <> Lazy1 constr
R14698:14707 Compounds <> Binary_op1 constr
R14712:14716 Compounds <> Lazy1 constr
R14727:14737 Compounds <> Ternary_op1 constr
R14742:14746 Compounds <> Lazy1 constr
R14757:14764 Compounds <> Unary_op constr
R14769:14773 Compounds <> Lazy1 constr
R14784:14788 Compounds <> Lazy2 constr
R14793:14797 Compounds <> Lazy1 constr
R14808:14812 Compounds <> Lazy1 constr
R14817:14821 Compounds <> Lazy1 constr
R14832:14837 Compounds <> Eager2 constr
R14842:14846 Compounds <> Lazy1 constr
R14857:14861 Compounds <> Eager constr
R14866:14870 Compounds <> Lazy1 constr
R14885:14889 Compounds <> Lazy1 constr
R14907:14912 Compounds <> status def
R14907:14912 Compounds <> status def
R15075:15077 Coq.Init.Logic <> :type_scope:x_'='_x not
R15050:15058 LamSF_Terms <> subst_rec def
R15071:15071 Coq.Init.Datatypes <> S constr
R15060:15063 Components <> star def
R15078:15081 Components <> star def
R15084:15092 LamSF_Terms <> subst_rec def
R15099:15099 Coq.Init.Datatypes <> S constr
R15102:15102 Coq.Init.Datatypes <> S constr
R15033:15037 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15041:15041 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15038:15038 Coq.Init.Datatypes <> S constr
R15020:15022 Coq.Init.Logic <> :type_scope:x_'='_x not
R15012:15017 Compounds <> status def
R15023:15025 Compounds <> Lam constr
R15075:15077 Coq.Init.Logic <> :type_scope:x_'='_x not
R15050:15058 LamSF_Terms <> subst_rec def
R15071:15071 Coq.Init.Datatypes <> S constr
R15060:15063 Components <> star def
R15078:15081 Components <> star def
R15084:15092 LamSF_Terms <> subst_rec def
R15099:15099 Coq.Init.Datatypes <> S constr
R15102:15102 Coq.Init.Datatypes <> S constr
R15033:15037 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15041:15041 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15038:15038 Coq.Init.Datatypes <> S constr
R15020:15022 Coq.Init.Logic <> :type_scope:x_'='_x not
R15012:15017 Compounds <> status def
R15023:15025 Compounds <> Lam constr
R15121:15148 Compounds <> subst_rec_preserves_star_lam thm
R15224:15226 Coq.Init.Logic <> :type_scope:x_'='_x not
R15199:15207 LamSF_Terms <> subst_rec def
R15220:15220 Coq.Init.Datatypes <> S constr
R15209:15212 Components <> star def
R15227:15230 Components <> star def
R15233:15241 LamSF_Terms <> subst_rec def
R15248:15248 Coq.Init.Datatypes <> S constr
R15251:15251 Coq.Init.Datatypes <> S constr
R15182:15186 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15190:15190 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15187:15187 Coq.Init.Datatypes <> S constr
R15166:15168 Coq.Init.Logic <> :type_scope:x_'='_x not
R15158:15163 Compounds <> status def
R15169:15174 Compounds <> Active constr
R15224:15226 Coq.Init.Logic <> :type_scope:x_'='_x not
R15199:15207 LamSF_Terms <> subst_rec def
R15220:15220 Coq.Init.Datatypes <> S constr
R15209:15212 Components <> star def
R15227:15230 Components <> star def
R15233:15241 LamSF_Terms <> subst_rec def
R15248:15248 Coq.Init.Datatypes <> S constr
R15251:15251 Coq.Init.Datatypes <> S constr
R15182:15186 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15190:15190 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R15187:15187 Coq.Init.Datatypes <> S constr
R15166:15168 Coq.Init.Logic <> :type_scope:x_'='_x not
R15158:15163 Compounds <> status def
R15169:15174 Compounds <> Active constr
R15270:15300 Compounds <> subst_rec_preserves_star_active thm
R15311:15320 Compounds <> factorable def
R15352:15357 Compounds <> status def
R15352:15357 Compounds <> status def
prf 15610:15641 <> subst_rec_preserves_components_l
R15657:15661 LamSF_Terms <> lamSF ind
R15718:15720 Coq.Init.Logic <> :type_scope:x_'='_x not
R15687:15695 LamSF_Terms <> subst_rec def
R15717:15717 Compounds <> k var
R15715:15715 Compounds <> n var
R15697:15710 Components <> left_component def
R15712:15712 Compounds <> M var
R15721:15734 Components <> left_component def
R15736:15744 LamSF_Terms <> subst_rec def
R15750:15750 Compounds <> k var
R15748:15748 Compounds <> n var
R15746:15746 Compounds <> M var
R15669:15678 Compounds <> factorable def
R15680:15680 Compounds <> M var
R15790:15799 Compounds <> factorable def
prf 15837:15875 <> subst_rec_preserves_components_active_r
R15892:15896 LamSF_Terms <> lamSF ind
R15982:15984 Coq.Init.Logic <> :type_scope:x_'='_x not
R15950:15958 LamSF_Terms <> subst_rec def
R15981:15981 Compounds <> k var
R15979:15979 Compounds <> N var
R15960:15974 Components <> right_component def
R15976:15976 Compounds <> M var
R15985:15999 Components <> right_component def
R16001:16009 LamSF_Terms <> subst_rec def
R16015:16015 Compounds <> k var
R16013:16013 Compounds <> N var
R16011:16011 Compounds <> M var
R15940:15942 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R15939:15939 Compounds <> i var
R15943:15943 Compounds <> k var
R15911:15913 Coq.Init.Logic <> :type_scope:x_'='_x not
R15903:15908 Compounds <> status def
R15910:15910 Compounds <> M var
R15914:15919 Compounds <> Active constr
R15921:15921 Compounds <> i var
R16174:16176 Coq.Init.Logic <> :type_scope:x_'='_x not
R16153:16161 LamSF_Terms <> subst_rec def
R16173:16173 Compounds <> k var
R16163:16166 Components <> star def
R16177:16180 Components <> star def
R16183:16191 LamSF_Terms <> subst_rec def
R16198:16198 Coq.Init.Datatypes <> S constr
R16200:16200 Compounds <> k var
R16141:16144 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R16140:16140 Compounds <> i var
R16145:16145 Compounds <> k var
R16125:16127 Coq.Init.Logic <> :type_scope:x_'='_x not
R16117:16122 Compounds <> status def
R16128:16133 Compounds <> Active constr
R16135:16135 Compounds <> i var
R16174:16176 Coq.Init.Logic <> :type_scope:x_'='_x not
R16153:16161 LamSF_Terms <> subst_rec def
R16173:16173 Compounds <> k var
R16163:16166 Components <> star def
R16177:16180 Components <> star def
R16183:16191 LamSF_Terms <> subst_rec def
R16198:16198 Coq.Init.Datatypes <> S constr
R16200:16200 Compounds <> k var
R16141:16144 Coq.Init.Peano <> :nat_scope:x_'<='_x not
R16140:16140 Compounds <> i var
R16145:16145 Compounds <> k var
R16125:16127 Coq.Init.Logic <> :type_scope:x_'='_x not
R16117:16122 Compounds <> status def
R16128:16133 Compounds <> Active constr
R16135:16135 Compounds <> i var
R16217:16247 Compounds <> subst_rec_preserves_star_active thm
R16271:16276 Compounds <> status def
R16271:16276 Compounds <> status def
prf 16327:16362 <> subst_rec_preserves_components_lam_r
R16379:16383 LamSF_Terms <> lamSF ind
R16466:16468 Coq.Init.Logic <> :type_scope:x_'='_x not
R16434:16442 LamSF_Terms <> subst_rec def
R16465:16465 Compounds <> k var
R16463:16463 Compounds <> N var
R16444:16458 Components <> right_component def
R16460:16460 Compounds <> M var
R16469:16483 Components <> right_component def
R16485:16493 LamSF_Terms <> subst_rec def
R16499:16499 Compounds <> k var
R16497:16497 Compounds <> N var
R16495:16495 Compounds <> M var
R16424:16426 Coq.Init.Peano <> :nat_scope:x_'<'_x not
R16423:16423 Compounds <> i var
R16427:16427 Compounds <> k var
R16398:16400 Coq.Init.Logic <> :type_scope:x_'='_x not
R16390:16395 Compounds <> status def
R16397:16397 Compounds <> M var
R16401:16403 Compounds <> Lam constr
R16405:16405 Compounds <> i var
R16563:16566 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R16551:16553 Coq.Init.Logic <> :type_scope:x_'='_x not
R16543:16548 Compounds <> status def
R16554:16556 Compounds <> Lam constr
R16559:16559 Coq.Init.Datatypes <> S constr
R16575:16577 Coq.Init.Logic <> :type_scope:x_'='_x not
R16567:16572 Compounds <> status def
R16578:16583 Compounds <> Active constr
R16586:16586 Coq.Init.Datatypes <> S constr
R16563:16566 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R16551:16553 Coq.Init.Logic <> :type_scope:x_'='_x not
R16543:16548 Compounds <> status def
R16554:16556 Compounds <> Lam constr
R16559:16559 Coq.Init.Datatypes <> S constr
R16575:16577 Coq.Init.Logic <> :type_scope:x_'='_x not
R16567:16572 Compounds <> status def
R16578:16583 Compounds <> Active constr
R16586:16586 Coq.Init.Datatypes <> S constr
R16606:16611 Compounds <> status def
R16606:16611 Compounds <> status def
R16664:16691 Compounds <> subst_rec_preserves_star_lam thm
R16698:16698 Coq.Init.Datatypes <> S constr
R16664:16691 Compounds <> subst_rec_preserves_star_lam thm
R16698:16698 Coq.Init.Datatypes <> S constr
R16723:16753 Compounds <> subst_rec_preserves_star_active thm
R16760:16760 Coq.Init.Datatypes <> S constr
R16723:16753 Compounds <> subst_rec_preserves_star_active thm
R16760:16760 Coq.Init.Datatypes <> S constr
prf 16790:16830 <> subst_rec_preserves_components_compound_r
R16847:16851 LamSF_Terms <> lamSF ind
R16919:16921 Coq.Init.Logic <> :type_scope:x_'='_x not
R16887:16895 LamSF_Terms <> subst_rec def
R16918:16918 Compounds <> k var
R16916:16916 Compounds <> n var
R16897:16911 Components <> right_component def
R16913:16913 Compounds <> M var
R16922:16936 Components <> right_component def
R16938:16946 LamSF_Terms <> subst_rec def
R16952:16952 Compounds <> k var
R16950:16950 Compounds <> n var
R16948:16948 Compounds <> M var
R16856:16865 Compounds <> factorable def
R16867:16867 Compounds <> M var
R17002:17011 Compounds <> factorable def
R17067:17070 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R17059:17061 Coq.Init.Logic <> :type_scope:x_'='_x not
R17051:17056 Compounds <> status def
R17062:17064 Compounds <> Lam constr
R17090:17093 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R17079:17081 Coq.Init.Logic <> :type_scope:x_'='_x not
R17071:17076 Compounds <> status def
R17082:17087 Compounds <> Active constr
R17094:17103 Compounds <> factorable def
R17067:17070 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R17059:17061 Coq.Init.Logic <> :type_scope:x_'='_x not
R17051:17056 Compounds <> status def
R17062:17064 Compounds <> Lam constr
R17090:17093 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R17079:17081 Coq.Init.Logic <> :type_scope:x_'='_x not
R17071:17076 Compounds <> status def
R17082:17087 Compounds <> Active constr
R17094:17103 Compounds <> factorable def
R17115:17124 Compounds <> factorable def
R17171:17176 Compounds <> status def
R17171:17176 Compounds <> status def
R17647:17649 Coq.Init.Logic <> :type_scope:x_'='_x not
R17211:17216 Compounds <> status def
R17234:17242 Compounds <> Reducible constr
R17247:17255 Compounds <> Reducible constr
R17266:17268 Compounds <> Lam constr
R17275:17279 Compounds <> Lazy1 constr
R17290:17292 Compounds <> Lam constr
R17295:17295 Coq.Init.Datatypes <> S constr
R17303:17305 Compounds <> Lam constr
R17318:17323 Compounds <> Active constr
R17330:17334 Compounds <> Lazy1 constr
R17345:17350 Compounds <> Active constr
R17353:17353 Coq.Init.Datatypes <> S constr
R17361:17363 Compounds <> Lam constr
R17376:17385 Compounds <> Ternary_op constr
R17390:17394 Compounds <> Lazy1 constr
R17405:17414 Compounds <> Binary_op0 constr
R17419:17423 Compounds <> Lazy1 constr
R17434:17443 Compounds <> Binary_op2 constr
R17448:17452 Compounds <> Lazy1 constr
R17463:17472 Compounds <> Binary_op1 constr
R17477:17481 Compounds <> Lazy1 constr
R17492:17502 Compounds <> Ternary_op1 constr
R17507:17511 Compounds <> Lazy1 constr
R17522:17529 Compounds <> Unary_op constr
R17534:17538 Compounds <> Lazy1 constr
R17549:17553 Compounds <> Lazy2 constr
R17558:17562 Compounds <> Lazy1 constr
R17573:17577 Compounds <> Lazy1 constr
R17582:17586 Compounds <> Lazy1 constr
R17597:17602 Compounds <> Eager2 constr
R17607:17611 Compounds <> Lazy1 constr
R17622:17626 Compounds <> Eager constr
R17631:17635 Compounds <> Lazy1 constr
R17650:17654 Compounds <> Lazy1 constr
R17647:17649 Coq.Init.Logic <> :type_scope:x_'='_x not
R17211:17216 Compounds <> status def
R17234:17242 Compounds <> Reducible constr
R17247:17255 Compounds <> Reducible constr
R17266:17268 Compounds <> Lam constr
R17275:17279 Compounds <> Lazy1 constr
R17290:17292 Compounds <> Lam constr
R17295:17295 Coq.Init.Datatypes <> S constr
R17303:17305 Compounds <> Lam constr
R17318:17323 Compounds <> Active constr
R17330:17334 Compounds <> Lazy1 constr
R17345:17350 Compounds <> Active constr
R17353:17353 Coq.Init.Datatypes <> S constr
R17361:17363 Compounds <> Lam constr
R17376:17385 Compounds <> Ternary_op constr
R17390:17394 Compounds <> Lazy1 constr
R17405:17414 Compounds <> Binary_op0 constr
R17419:17423 Compounds <> Lazy1 constr
R17434:17443 Compounds <> Binary_op2 constr
R17448:17452 Compounds <> Lazy1 constr
R17463:17472 Compounds <> Binary_op1 constr
R17477:17481 Compounds <> Lazy1 constr
R17492:17502 Compounds <> Ternary_op1 constr
R17507:17511 Compounds <> Lazy1 constr
R17522:17529 Compounds <> Unary_op constr
R17534:17538 Compounds <> Lazy1 constr
R17549:17553 Compounds <> Lazy2 constr
R17558:17562 Compounds <> Lazy1 constr
R17573:17577 Compounds <> Lazy1 constr
R17582:17586 Compounds <> Lazy1 constr
R17597:17602 Compounds <> Eager2 constr
R17607:17611 Compounds <> Lazy1 constr
R17622:17626 Compounds <> Eager constr
R17631:17635 Compounds <> Lazy1 constr
R17650:17654 Compounds <> Lazy1 constr
R17671:17676 Compounds <> status def
R17671:17676 Compounds <> status def
R17742:17751 Compounds <> factorable def
R17767:17772 Compounds <> status def
R17767:17772 Compounds <> status def
R17842:17869 Compounds <> subst_rec_preserves_star_lam thm
R17842:17869 Compounds <> subst_rec_preserves_star_lam thm
R17916:17946 Compounds <> subst_rec_preserves_star_active thm
R17916:17946 Compounds <> subst_rec_preserves_star_active thm
R17978:18012 Compounds <> subst_rec_preserves_star_factorable thm
R17978:18012 Compounds <> subst_rec_preserves_star_factorable thm
def 18056:18073 <> preserves_compound
R18080:18086 LamSF_Tactics <> termred def
R18150:18153 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R18140:18147 Compounds <> compound def
R18149:18149 Compounds <> N var
R18195:18198 Coq.Init.Logic <> :type_scope:x_'/\'_x not
R18154:18156 Compounds <> red var
R18178:18191 Components <> left_component def
R18193:18193 Compounds <> N var
R18159:18172 Components <> left_component def
R18174:18174 Compounds <> M var
R18199:18201 Compounds <> red var
R18223:18237 Components <> right_component def
R18239:18239 Compounds <> N var
R18203:18217 Components <> right_component def
R18219:18219 Compounds <> M var
R18128:18130 Compounds <> red var
R18134:18134 Compounds <> N var
R18132:18132 Compounds <> M var
R18104:18111 Compounds <> compound def
R18113:18113 Compounds <> M var
prf 18251:18272 <> preserves_compound_seq
R18295:18301 LamSF_Tactics <> termred def
R18388:18405 Compounds <> preserves_compound def
R18408:18417 LamSF_Tactics <> sequential ind
R18424:18427 Compounds <> red2 var
R18419:18422 Compounds <> red1 var
R18332:18349 Compounds <> preserves_compound def
R18351:18354 Compounds <> red2 var
R18305:18322 Compounds <> preserves_compound def
R18324:18327 Compounds <> red1 var
R18597:18603 LamSF_Tactics <> seq_red constr
R18689:18695 LamSF_Tactics <> seq_red constr
prf 18713:18741 <> preserves_compound_multi_step
R18758:18764 LamSF_Tactics <> termred def
R18794:18811 Compounds <> preserves_compound def
R18814:18823 LamSF_Tactics <> multi_step ind
R18825:18827 Compounds <> red var
R18768:18785 Compounds <> preserves_compound def
R18787:18789 Compounds <> red var
R18937:18950 Components <> left_component def
R18922:18929 LamSF_Tactics <> succ_red constr
R18937:18950 Components <> left_component def
R18922:18929 LamSF_Tactics <> succ_red constr
R19020:19034 Components <> right_component def
R19005:19012 LamSF_Tactics <> succ_red constr
R19020:19034 Components <> right_component def
R19005:19012 LamSF_Tactics <> succ_red constr
R19103:19131 Compounds <> preserves_compound_multi_step thm
prf 19143:19171 <> lift_rec_preserves_factorable
R19205:19214 Compounds <> factorable def
R19217:19224 LamSF_Terms <> lift_rec def
R19230:19230 Compounds <> k var
R19228:19228 Compounds <> n var
R19226:19226 Compounds <> M var
R19189:19198 Compounds <> factorable def
R19200:19200 Compounds <> M var
R19281:19283 Coq.Init.Logic <> :type_scope:x_'='_x not
R19258:19263 Compounds <> status def
R19266:19273 LamSF_Terms <> lift_rec def
R19284:19298 Compounds <> relocate_status def
R19301:19306 Compounds <> status def
R19281:19283 Coq.Init.Logic <> :type_scope:x_'='_x not
R19258:19263 Compounds <> status def
R19266:19273 LamSF_Terms <> lift_rec def
R19284:19298 Compounds <> relocate_status def
R19301:19306 Compounds <> status def
R19328:19352 Compounds <> lift_rec_preserves_status thm
R19363:19372 Compounds <> factorable def
prf 19719:19748 <> subst_rec_preserves_factorable
R19790:19799 Compounds <> factorable def
R19802:19810 LamSF_Terms <> subst_rec def
R19816:19816 Compounds <> k var
R19814:19814 Compounds <> N var
R19812:19812 Compounds <> M var
R19762:19771 Compounds <> factorable def
R19773:19773 Compounds <> M var
R19899:19901 Coq.Init.Logic <> :type_scope:x_'='_x not
R19875:19880 Compounds <> status def
R19883:19891 LamSF_Terms <> subst_rec def
R19902:19907 Compounds <> status def
R19899:19901 Coq.Init.Logic <> :type_scope:x_'='_x not
R19875:19880 Compounds <> status def
R19883:19891 LamSF_Terms <> subst_rec def
R19902:19907 Compounds <> status def
R19924:19949 Compounds <> subst_rec_preserves_status thm
R19971:19980 Compounds <> factorable def
R20060:20062 Coq.Init.Logic <> :type_scope:x_'='_x not
R20036:20041 Compounds <> status def
R20044:20052 LamSF_Terms <> subst_rec def
R20063:20068 Compounds <> status def
R20060:20062 Coq.Init.Logic <> :type_scope:x_'='_x not
R20036:20041 Compounds <> status def
R20044:20052 LamSF_Terms <> subst_rec def
R20063:20068 Compounds <> status def
R20085:20110 Compounds <> subst_rec_preserves_status thm
R20132:20141 Compounds <> factorable def
R20222:20224 Coq.Init.Logic <> :type_scope:x_'='_x not
R20198:20203 Compounds <> status def
R20206:20214 LamSF_Terms <> subst_rec def
R20225:20230 Compounds <> status def
R20222:20224 Coq.Init.Logic <> :type_scope:x_'='_x not
R20198:20203 Compounds <> status def
R20206:20214 LamSF_Terms <> subst_rec def
R20225:20230 Compounds <> status def
R20247:20272 Compounds <> subst_rec_preserves_status thm
R20294:20303 Compounds <> factorable def
R20384:20386 Coq.Init.Logic <> :type_scope:x_'='_x not
R20360:20365 Compounds <> status def
R20368:20376 LamSF_Terms <> subst_rec def
R20387:20392 Compounds <> status def
R20384:20386 Coq.Init.Logic <> :type_scope:x_'='_x not
R20360:20365 Compounds <> status def
R20368:20376 LamSF_Terms <> subst_rec def
R20387:20392 Compounds <> status def
R20409:20434 Compounds <> subst_rec_preserves_status thm
R20456:20465 Compounds <> factorable def
R20546:20548 Coq.Init.Logic <> :type_scope:x_'='_x not
R20522:20527 Compounds <> status def
R20530:20538 LamSF_Terms <> subst_rec def
R20549:20554 Compounds <> status def
R20546:20548 Coq.Init.Logic <> :type_scope:x_'='_x not
R20522:20527 Compounds <> status def
R20530:20538 LamSF_Terms <> subst_rec def
R20549:20554 Compounds <> status def
R20571:20596 Compounds <> subst_rec_preserves_status thm
R20618:20627 Compounds <> factorable def
R20708:20710 Coq.Init.Logic <> :type_scope:x_'='_x not
R20684:20689 Compounds <> status def
R20692:20700 LamSF_Terms <> subst_rec def
R20711:20716 Compounds <> status def
R20708:20710 Coq.Init.Logic <> :type_scope:x_'='_x not
R20684:20689 Compounds <> status def
R20692:20700 LamSF_Terms <> subst_rec def
R20711:20716 Compounds <> status def
R20733:20758 Compounds <> subst_rec_preserves_status thm
R20780:20789 Compounds <> factorable def
R20842:20844 Coq.Init.Logic <> :type_scope:x_'='_x not
R20818:20823 Compounds <> status def
R20826:20834 LamSF_Terms <> subst_rec def
R20845:20850 Compounds <> status def
R20842:20844 Coq.Init.Logic <> :type_scope:x_'='_x not
R20818:20823 Compounds <> status def
R20826:20834 LamSF_Terms <> subst_rec def
R20845:20850 Compounds <> status def
R20867:20892 Compounds <> subst_rec_preserves_status thm
R20966:20975 Compounds <> factorable def
prf 21011:21027 <> status_app_active
R21096:21099 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R21085:21087 Coq.Init.Logic <> :type_scope:x_'='_x not
R21077:21082 Compounds <> status def
R21084:21084 Compounds <> M var
R21088:21093 Compounds <> Active constr
R21095:21095 Compounds <> i var
R21119:21122 Coq.Init.Logic <> :type_scope:x_'\/'_x not
R21108:21110 Coq.Init.Logic <> :type_scope:x_'='_x not
R21100:21105 Compounds <> status def
R21107:21107 Compounds <> N var
R21111:21116 Compounds <> Active constr
R21118:21118 Compounds <> i var
R21131:21133 Coq.Init.Logic <> :type_scope:x_'='_x not
R21123:21128 Compounds <> status def
R21130:21130 Compounds <> N var
R21134:21136 Compounds <> Lam constr
R21138:21138 Compounds <> i var
R21061:21063 Coq.Init.Logic <> :type_scope:x_'='_x not
R21045:21050 Compounds <> status def
R21053:21055 LamSF_Terms <> App constr
R21059:21059 Compounds <> N var
R21057:21057 Compounds <> M var
R21064:21069 Compounds <> Active constr
R21071:21071 Compounds <> i var
R21212:21217 Compounds <> status def
R21212:21217 Compounds <> status def
R21253:21258 Compounds <> status def
R21253:21258 Compounds <> status def
R21300:21305 Compounds <> status def
R21325:21330 Compounds <> status def
R21349:21354 Compounds <> status def
R21300:21305 Compounds <> status def
R21325:21330 Compounds <> status def
R21325:21330 Compounds <> status def
R21325:21330 Compounds <> status def
R21325:21330 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
R21349:21354 Compounds <> status def
prf 21385:21411 <> lift_rec_preserves_compound
R21443:21450 Compounds <> compound def
R21453:21460 LamSF_Terms <> lift_rec def
R21466:21466 Compounds <> k var
R21464:21464 Compounds <> n var
R21462:21462 Compounds <> M var
R21429:21436 Compounds <> compound def
R21438:21438 Compounds <> M var
R21517:21519 Coq.Init.Logic <> :type_scope:x_'='_x not
R21494:21499 Compounds <> status def
R21502:21509 LamSF_Terms <> lift_rec def
R21520:21534 Compounds <> relocate_status def
R21537:21542 Compounds <> status def
R21517:21519 Coq.Init.Logic <> :type_scope:x_'='_x not
R21494:21499 Compounds <> status def
R21502:21509 LamSF_Terms <> lift_rec def
R21520:21534 Compounds <> relocate_status def
R21537:21542 Compounds <> status def
R21564:21588 Compounds <> lift_rec_preserves_status thm
R21599:21606 Compounds <> compound def
prf 21742:21769 <> subst_rec_preserves_compound
R21809:21816 Compounds <> compound def
R21819:21827 LamSF_Terms <> subst_rec def
R21833:21833 Compounds <> k var
R21831:21831 Compounds <> N var
R21829:21829 Compounds <> M var
R21783:21790 Compounds <> compound def
R21792:21792 Compounds <> M var
R21864:21873 Compounds <> factorable def
R21864:21873 Compounds <> factorable def
R21889:21912 Compounds <> compounds_are_factorable thm
R21923:21932 Compounds <> factorable def
R21935:21943 LamSF_Terms <> subst_rec def
R21923:21932 Compounds <> factorable def
R21935:21943 LamSF_Terms <> subst_rec def
R21964:21993 Compounds <> subst_rec_preserves_factorable thm
R22002:22040 Compounds <> factorable_implies_compound_or_operator thm
R22043:22051 LamSF_Terms <> subst_rec def
R22002:22040 Compounds <> factorable_implies_compound_or_operator thm
R22043:22051 LamSF_Terms <> subst_rec def
R22100:22107 Compounds <> compound def