X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpmuwe.ma;h=99eb4d4becf6da685655fbafba902614f19f6d0f;hp=ce73661f85265d67aab1ee1b03d715b05d23ddf9;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
index ce73661f8..99eb4d4be 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma
@@ -27,7 +27,7 @@ lemma cnv_cpmuwe_trans (h) (a) (G) (L):
 
 lemma cnv_R_cpmuwe_total (h) (a) (G) (L):
       ∀T1. ❪G,L❫ ⊢ T1 ![h,a] → ∃n. R_cpmuwe h G L T1 n.
-/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-.
+/4 width=3 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-.
 
 (* Main inversions with head evaluation for t-bound rt-transition on terms **)