X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs_csx.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs_csx.ma;h=ce44e7e7bb20687d5374f380db3852294db97f6a;hb=f129bbbfda0e65a5f92ec086246f6e288376d4f9;hp=a15e715f1169bb6b7910f8222e0e3affe0276f4d;hpb=54c4e854515cbcb1376881e9aedad006bf6545f2;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma index a15e715f1..ce44e7e7b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/fpbs.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) -(* Properties with sn for uncounted parallel rt-transition for terms ********) +(* Properties with sn for unbound parallel rt-transition for terms **********) (* Basic_2A1: was: csx_fpbs_conf *) lemma fpbs_csx_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →