- intermediate commit to allow debugging of auto tactic in xprs.ma

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / equivalence / cpcs_cpcs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
index fcad182e0a2d88d63133ee160fab9fceee530fa1..31a8d0b49c77e593a8b0662472d09da094874508 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
@@ -83,13 +83,28 @@ lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                      L ⊢ U1 ⬌* U2 → K ⊢ T1 ⬌* T2.
 #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
 elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
-elim (cprs_inv_lift … HLK … HTU1 … HU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift … HLK … HTU2 … HU2) -L -U2 #X #HXU
+elim (cprs_inv_lift1 … HLK … HTU1 … HU1) -U1 #T #HTU #HT1
+elim (cprs_inv_lift1 … HLK … HTU2 … HU2) -L -U2 #X #HXU
 >(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/
 qed-.
 
 (* Advanced properties ******************************************************)
 
+lemma cpr_cprs_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_strip … HT1 … HT2) /2 width=3 by cpr_cprs_div/
+qed-.
+
+lemma cprs_cpr_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡ T2 → L ⊢ T2 ⬌* T1.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_strip … HT1 … HT2) /2 width=3 by cprs_cpr_div/
+qed-.
+
+lemma cprs_conf: ∀L,T,T1,T2. L ⊢ T ➡* T1 → L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
+#L #T #T1 #T2 #HT1 #HT2
+elim (cprs_conf … HT1 … HT2) /2 width=3/
+qed-.
+
 (* Basic_1: was only: pc3_thin_dx *)
 lemma cpcs_flat: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
                  ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2.