some renaming and some typos corrected ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
index 6b998fb131999f8cc104dacc5ada63d1a276461b..65a6146a7854dbe6dce6b3335ff9443e7dd2dbd3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
@@ -24,7 +24,7 @@ definition cpre: relation4 genv lenv term term ≝
 interpretation "evaluation for context-sensitive parallel reduction (term)"
    'PRedEval G L T1 T2 = (cpre G L T1 T2).
 
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
 
 (* Basic_1: was just: nf2_sn3 *)
 lemma csx_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄.