(* *)
(**************************************************************************)
-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 ***************)
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
qed-.
(*
(* Basic_2A1: was: cpx_lleq_conf *)
-lemma cpx_req_conf: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
- ∀L1. L2 ≘[T1] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h] T2.
+lemma cpx_req_conf: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
+ ∀L1. L2 ≘[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
/3 width=3 by req_cpx_trans, req_sym/ qed-.
*)
(* Basic_2A1: was: cpx_lleq_conf_sn *)
/2 width=5 by cpx_rex_conf/ qed-.
(*
(* Basic_2A1: was: cpx_lleq_conf_dx *)
-lemma cpx_req_conf_dx: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
+lemma cpx_req_conf_dx: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
∀L1. L1 ≘[T1] L2 → L1 ≘[T2] L2.
/4 width=6 by cpx_req_conf_sn, req_sym/ qed-.
*)