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_req.ma;h=b0d2b9922cbacc2ec13dd63e7916f95797708256;hp=a836bfbea26c650a703cd6c3c1eceb686127510e;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hpb=d71e53021b0c17e1a00c2d623e7139c6d18069d5

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
index a836bfbea..b0d2b9922 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/static/req.ma".
+include "static_2/static/req_drops.ma".
 include "basic_2/rt_transition/rpx_fsle.ma".
 
 (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
@@ -32,8 +32,10 @@ lemma req_cpx_trans: ∀h,G. req_transitive (cpx h G).
   elim (req_inv_bind … H) -H /3 width=1 by cpx_bind/
 | #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H
   elim (req_inv_flat … H) -H /3 width=1 by cpx_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IH #L1 #H
-  elim (req_inv_bind … H) -H /3 width=3 by cpx_zeta/
+| #G #L2 #V2 #T1 #T #T2 #HT1 #_ #IH #L1 #H
+  elim (req_inv_bind … H) -H #HV2 #H
+  lapply (req_inv_lifts_bi … H (Ⓣ) … HT1) -H [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT
+  /3 width=3 by cpx_zeta/
 | #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H
   elim (req_inv_flat … H) -H /3 width=1 by cpx_eps/
 | #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H