this is the real update :)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / equivalence / fpcs_cpcs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
index 75e69cf083a8ee38f1d141529b9c1d3ef742170a..b1288f7514a1009ca4d494db119a24abcdbf887f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs_cpcs.ma
@@ -20,6 +20,13 @@ include "basic_2/equivalence/fpcs_fpcs.ma".
 
 (* Advanced properties ******************************************************)
 
+lemma fpcs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 →
+                        ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ⬌* ⦃L2, ⓕ{I}V2.T2⦄.
+#L1 #L2 #T1 #T2 #HT12
+elim (fpcs_inv_fprs … HT12) -HT12
+/3 width=6 by fprs_flat_dx_tpr, fprs_div/ (**) (* auto too slow without trace *)
+qed.
+
 lemma fpcs_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄ →
                   ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄.
 #I #L1 #L2 #V1 #V2 #T1 #T2 #H12
@@ -31,7 +38,7 @@ qed.
 (* Advanced inversion lemmas ************************************************)
 
 lemma fpcs_inv_shift: ∀I,L1,L2,V1,V2,T1,T2. ⦃L1.ⓑ{I}V1, T1⦄ ⬌* ⦃L2.ⓑ{I}V2, T2⦄ →
-                         ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄.
+                      ⦃L1, -ⓑ{I}V1.T1⦄ ⬌* ⦃L2, -ⓑ{I}V2.T2⦄.
 #I #L1 #L2 #V1 #V2 #T1 #T2 #H12
 elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2
 elim (fprs_inv_pair1 … H1) -H1 #K1 #U1 #_ #HTU1 #H destruct