X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpx.ma;h=3da67484aaa0d1f427d6cb6decbcb85a7b363226;hp=2e657b0270f01be183537fdaa81971e09bf84119;hb=19a25bf176255055193372554437729a6fa1894c;hpb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
index 2e657b027..3da67484a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
@@ -100,6 +100,12 @@ lemma cpx_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
 #h * /2 width=2 by cpx_flat, cpx_bind/
 qed.
 
+lemma cpg_cpx (h) (Rt) (c) (G) (L):
+              ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → ⦃G,L⦄ ⊢ T1 ⬈[h] T2.
+#h #Rt #c #G #L #T1 #T2 #H elim H -c -G -L -T1 -T2
+/2 width=3 by cpx_theta, cpx_beta, cpx_ee, cpx_eps, cpx_zeta, cpx_flat, cpx_bind, cpx_lref, cpx_delta/
+qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma cpx_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[h] T2 →