X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fequivalence%2Fcpcs_cprs.ma;h=cb1f5d76ac1e0f92f2d4ceebc2abf537f4ace572;hb=4bea40e6589ce21c15ecf99bdd5bd2a1c62f6809;hp=7394858efe4b089cd987a9f4d383bb62e49235db;hpb=fde3b3d2e6cc48f6c9880136b1a0d565e2c78c1f;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
index 7394858ef..cb1f5d76a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
@@ -24,17 +24,11 @@ lemma cpcs_cprs_dx: ∀L,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/
 qed.
 
-lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
-
 (* Basic_1: was: pc3_pr3_x *)
 lemma cpcs_cprs_sn: ∀L,T1,T2. L ⊢ T2 ➡* T1 → L ⊢ T1 ⬌* T2.
 #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/
 qed.
 
-lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
-
 lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/
 qed.
@@ -57,3 +51,9 @@ qed.
 lemma cprs_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
 #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=1/ /2 width=3/
 qed.
+
+lemma cprs_cpr_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
+/3 width=5 by step, cprs_div/ qed-.
+
+lemma cpr_cprs_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
+/3 width=3 by step, cprs_div/ qed-.