X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freducibility%2Flcpr.ma;h=80d14a2e516f5e62a0befb1cccc3def5027f7fb5;hb=70ac3a792389497103fb80b5a1a144706addb7cb;hp=13545ad849e7fd98105695808bef8481146c36f4;hpb=f75be90562ddd964ef7ed43b956eb908f3133e3a;p=helm.git

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 13545ad84..80d14a2e5 100644
--- 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. ∃∃L. L1 ⇒ L & L [0, |L|] ≫* L2
+   λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶* L2
 .
 
 interpretation
@@ -27,11 +27,11 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma lcpr_refl: ∀L. L ⊢ ⇒ L.
-/2/ qed.
+lemma lcpr_refl: ∀L. L ⊢ ➡ L.
+/2 width=3/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ⇒ L2 → L2 = ⋆.
+lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
 #L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
 qed-.