slight refactoring in the proof of strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csx_lift.ma

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 ade57bbd9271c71e32d436f19b2fe2cbb6f8db09..d12f16a77e8f61b9890918c01ac8f4110341a8f3 100644 (file)
--- 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.