X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpre_cpre.ma;h=5ddc528f4367d3a83f998accc7392fad8c9ab39a;hp=202e1ccad0c3897b9d5ea9ef95508af3e2fc9441;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma
index 202e1ccad..5ddc528f4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma
@@ -32,7 +32,7 @@ qed-.
 
 (* Basic_1: was: nf2_pr3_confluence *)
 theorem cpre_mono (h) (G) (L) (T):
-        ∀T1. ⦃G, L⦄ ⊢ T ➡*[h] 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] 𝐍⦃T2⦄ → T1 = T2.
+        ∀T1. ⦃G,L⦄ ⊢ T ➡*[h] 𝐍⦃T1⦄ → ∀T2. ⦃G,L⦄ ⊢ T ➡*[h] 𝐍⦃T2⦄ → T1 = T2.
 #h #G #L #T0 #T1 * #HT01 #HT1 #T2 * #HT02 #HT2
 elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20
 >(cprs_inv_cnr_sn … HT10 HT1) -T1