(* *)
(**************************************************************************)
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/substitution/drop_drop.ma".
include "basic_2/multiple/frees.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
[ -n @or_intror #H elim (lt_refl_false i)
lapply (frees_inv_lref_skip … H ?) -L //
| elim (lt_or_ge j (|L|)) #Hj
- [ elim (ldrop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
- elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, ldrop_fwd_rfw, or_introl/ ] #HnW
+ [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
+ elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
@or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -d
- lapply (ldrop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
+ lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
| -n @or_intror #H elim (lt_refl_false i)
lapply (frees_inv_lref_free … H ?) -d //
]
elim (le_to_or_lt_eq … Hdj) -Hdj
[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
| -Hji -HnU #H destruct
- lapply (ldrop_mono … HLK0 … HLK) #H destruct -I
+ lapply (drop_mono … HLK0 … HLK) #H destruct -I
elim HnW0 -L -U -HnW0 //
]
qed.
@frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
| #I #K #K0 #T #V #d #i #j #Hdj #Hji #HnT #HK0 #HV #IHV #L #s #d0 #e0 #HLK #U #HTU #Hd0i
elim (lt_or_ge j d0) #H1
- [ elim (ldrop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
+ [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
@(frees_be … HL0) -HL0 -HV
/3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/
[ #X #HXU >(plus_minus_m_m d0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU
| >minus_plus <plus_minus // <minus_plus
/3 width=5 by monotonic_le_minus_l2/
]
- | lapply (ldrop_trans_ge … HLK … HK0 ?) // -K #HLK0
- lapply (ldrop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
+ | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
+ lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
@(frees_be … HLK0) -HLK0 -IHV
/2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/
#X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
elim (lift_split … HTU i e0) -HTU /2 width=2 by/
| #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hd0i #Hide0
elim (lt_or_ge j d0) #H1
- [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+ [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
@(IHW … HKL0 … HVW)
[ /2 width=1 by monotonic_le_minus_l2/
| >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
| #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hde0i
elim (lt_or_ge j d0) #H1
- [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+ [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
elim (le_inv_plus_l … Hde0i) #H0 #He0i
@(frees_be … H) -H
[ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
#X #_ #H elim (HnU … H)
| >commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/
]
- | lapply (ldrop_conf_ge … HLK … HLK0 ?) // -L #HK0
+ | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
elim (le_inv_plus_l … H2) -H2 #H2 #He0j
@(frees_be … HK0)
[ /2 width=1 by monotonic_yle_minus_dx/