partial commit of the components before "conversion"

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lprs_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
index 3a7475d0a1fe88901c17b743728393848b8b0038..508b306d3907515c7fdab6e553a9aac00d6dce32 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma
@@ -23,17 +23,17 @@ definition lprsa: relation lenv ≝ lpx_sn … cprs.
 interpretation "parallel computation (local environment, sn variant) alternative"
    'PRedSnStarAlt L1 L2 = (lprsa L1 L2).
 
-(* Main properties on the alternative definition **********************************)
+(* Main properties on the alternative definition ****************************)
 
 theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2.
 /2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
 
-(* Main inversion lemmas on the alternative definition ****************************)
+(* Main inversion lemmas on the alternative definition **********************)
 
 theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2.
 /3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-.
 
-(* Alternative eliminators ********************************************************)
+(* Alternative eliminators **************************************************)
 
 lemma lprs_ind_alt: ∀R:relation lenv.
                     R (⋆) (⋆) → (