- some work on extensions:

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
index 92b694f91ea311075d06391d7f97f32b4a1a17a9..de9a897b913798991585e8a23a7f3ebb0996a710 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/substitution/fqus_fqus.ma".
 include "basic_2/unfold/lsstas_lift.ma".
-include "basic_2/reduction/llpx_ldrop.ma".
+include "basic_2/reduction/cpx_lift.ma".
 include "basic_2/computation/cpxs.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
@@ -42,9 +42,6 @@ lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i.
 ]
 qed.
 
-lemma cpxs_llpx_conf: ∀h,g,G. s_r_confluent1 … (cpxs h g G) (llpx h g G 0).
-/3 width=5 by llpx_cpx_conf, s_r_conf1_LTC1/ qed-.
-
 (* Advanced inversion lemmas ************************************************)
 
 lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →