X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs.ma;h=ae0c1ae627ecc8cf4e95ba20bce361f79d7a155e;hb=eae50cc815292d335df1c488a00b39ef98fa5870;hp=dbd23a0a47821e949c2e100529bf5fc001f2d31d;hpb=cb38da6095e3af84131a3ebf47a9f252f34a804c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
index dbd23a0a4..ae0c1ae62 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/cnf.ma".
+include "basic_2/computation/tprs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
 
@@ -55,8 +56,8 @@ lemma cprs_strap2: ∀L,T1,T,T2.
 /2 width=3/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
-                       ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡* T2.
+lemma cprs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+                        ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
 /3 width=3/
 qed.
 
@@ -68,6 +69,11 @@ lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2
 @(cprs_strap1 … IHT2) -IHT2 /2 width=1/
 qed.
 
+(* Basic_1: was: pr3_pr1 *)
+lemma tprs_cprs: ∀T1,T2. T1 ➡* T2 → ∀L. L ⊢ T1 ➡* T2.
+#T1 #T2 #H @(tprs_ind … H) -T2 /2 width=1/ /3 width=3/
+qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 (* Basic_1: was: pr3_gen_sort *)
@@ -94,6 +100,9 @@ lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U.
 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
 qed-.
 
+lemma tprs_inv_cnf1: ∀T,U. T ➡* U → ⋆ ⊢ 𝐍⦃T⦄ → T = U.
+/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-.
+
 (* Basic_1: removed theorems 10:
    clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12