lambdadelta

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index 028798162fbfaecb0d47a9a2fa1971f7ec2e666d..c8f64f148376391f4dfb8cd19404b6c53b8dbe65 100644 (file)
--- 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.