milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpmuwe.ma

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 ce73661f85265d67aab1ee1b03d715b05d23ddf9..99eb4d4becf6da685655fbafba902614f19f6d0f 100644 (file)
--- 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 **)