- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 40608cf5cc5aa261a77e4707a4e4d569f158b56b..e20ce0559c9639a07234ac19a1f0511533883e13 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -17,7 +17,6 @@ include "basic_2/computation/tprs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
 
-(* Basic_1: includes: pr3_pr2 *)
 definition cprs: lenv → relation term ≝
                  λL. TC … (cpr L).
 
@@ -42,6 +41,10 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+(* Basic_1: was: pr3_pr2 *)
+lemma cpr_cprs: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ➡* T2.
+/2 width=1/ qed.
+
 (* Basic_1: was: pr3_refl *)
 lemma cprs_refl: ∀L,T. L ⊢ T ➡* T.
 /2 width=1/ qed.