X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freducibility%2Ffpr_cpr.ma;h=007681d0bc410f76fea0d57c3ea7020ebbc939dc;hb=18bc3082b332504f60345245e716b62ae628e3a7;hp=a6f57bbf9f673dc2ba0135fb66eaaa9197d803ba;hpb=18df696e2c97546e5d42e86d18691b8546339160;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
index a6f57bbf9..007681d0b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma
@@ -36,11 +36,17 @@ elim (le_or_ge (|K|) d) #Hd
 [ elim (ldrop_ltpss_sn_trans_ge … HLK … HK2 …)
 | elim (ldrop_ltpss_sn_trans_be … HLK … HK2 …)
 ] // -Hd #L2 #HL2 #HLK2
-lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/ 
+lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/
 qed-.
 
 (* Advanced properties ******************************************************)
 
+lemma fpr_flat_dx: ∀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 (fpr_inv_all … HT12) -HT12 /4 width=4/
+qed.
+
 lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
                    ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
 #L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I