X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsx_lift.ma;h=d12f16a77e8f61b9890918c01ac8f4110341a8f3;hb=33f8507cadd3b36dc9afa227d8968dda66fe2034;hp=ade57bbd9271c71e32d436f19b2fe2cbb6f8db09;hpb=01efd2c88dd65ba5dbf9c946000b5d03a98acad8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
index ade57bbd9..d12f16a77 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
@@ -111,8 +111,9 @@ qed-.
 
 theorem csx_gcp: ∀h,g. gcp (cpx h g) (eq …) (csx h g).
 #h #g @mk_gcp
-[ /3 width=13 by cnx_lift/
+[ normalize /3 width=13 by cnx_lift/
 | #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/
+| /2 width=8 by csx_lift/
 | /2 width=3 by csx_fwd_flat_dx/
 ]
 qed.