X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcpxs.ma;h=c8f64f148376391f4dfb8cd19404b6c53b8dbe65;hb=65008df95049eb835941ffea1aa682c9253c4c2b;hp=028798162fbfaecb0d47a9a2fa1971f7ec2e666d;hpb=c07e9b0a3e65c28ca4154fec76a54a9a118fa7e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index 028798162..c8f64f148 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/predstar_5.ma".
 include "basic_2/reduction/cnx.ma".
 include "basic_2/computation/cprs.ma".
 
@@ -59,11 +60,10 @@ lemma lsubx_cpxs_trans: ∀h,g. lsub_trans … (cpxs h g) lsubx.
 /3 width=5 by lsubx_cpx_trans, TC_lsub_trans/
 qed-.
 
-axiom cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
-(*
+lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
 #h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
 qed.
-*)
+
 lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
                     ∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 →
                     ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.