- notation fix for reducible and normal forms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / reducibility / lcpr.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma
index 13545ad849e7fd98105695808bef8481146c36f4..80d14a2e516f5e62a0befb1cccc3def5027f7fb5 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma
@@ -18,7 +18,7 @@ include "Basic_2/reducibility/ltpr.ma".
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
 
 definition lcpr: relation lenv ≝
-   λL1,L2. â\88\83â\88\83L. L1 â\87\92 L & L [0, |L|] â\89«* L2
+   λL1,L2. â\88\83â\88\83L. L1 â\9e¡ L & L [0, |L|] â\96¶* L2
 .
 
 interpretation
@@ -27,11 +27,11 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma lcpr_refl: â\88\80L. L â\8a¢ â\87\92 L.
-/2/ qed.
+lemma lcpr_refl: â\88\80L. L â\8a¢ â\9e¡ L.
+/2 width=3/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lcpr_inv_atom1: â\88\80L2. â\8b\86 â\8a¢ â\87\92 L2 → L2 = ⋆.
+lemma lcpr_inv_atom1: â\88\80L2. â\8b\86 â\8a¢ â\9e¡ L2 → L2 = ⋆.
 #L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
 qed-.