X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpx.ma;h=c0ca76840f32238d9fdeb0438d47313eab8333d7;hb=984856dbab870ddc3156040df69b1f1846cc3aaf;hp=57c0184beedb536c36ad05b3ccc961fdff564be9;hpb=45996e63afdb9802935990660c4912d58035e016;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
index 57c0184be..c0ca76840 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
@@ -46,6 +46,12 @@ lemma lfpx_gref: ∀h,I,G,L1,L2,V1,V2,l.
                  ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, §l] L2.ⓑ{I}V2.
 /2 width=1 by lfxs_gref/ qed.
 
+lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1.
+                         ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V1 →
+                         ∀V2. ⦃G, L1⦄ ⊢ V ⬈[h] V2 →
+                         ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V2.
+/2 width=2 by lfxs_pair_repl_dx/ qed-.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma lfpx_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] Y2 → Y2 = ⋆.