X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsx_lift.ma;h=ade57bbd9271c71e32d436f19b2fe2cbb6f8db09;hb=fca909e9e53de73771e1b47e94434ae8f747d7fb;hp=f8111465638dc8ffca685fdeb2d6f260b34d519a;hpb=795ac6cc4ef54b4470b5e2fba287acca440c9c18;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 f81114656..ade57bbd9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/reduction/cnx_lift.ma".
-include "basic_2/computation/acp.ma".
+include "basic_2/computation/gcp.ma".
 include "basic_2/computation/csx.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
@@ -109,8 +109,8 @@ qed-.
 
 (* Main properties **********************************************************)
 
-theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g).
-#h #g @mk_acp
+theorem csx_gcp: ∀h,g. gcp (cpx h g) (eq …) (csx h g).
+#h #g @mk_gcp
 [ /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=3 by csx_fwd_flat_dx/