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=64207d0b4d80bcedcfbae0526ce635e993f027a7;hp=0891cb00cef0fbf84140658716b94c82d9bb5528;hpb=ea83c19f4cac864dd87eb059d8aeb2343eba480f;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 0891cb00c..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 **************************)
 
@@ -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