(**************************************************************************)
include "basic_2/multiple/fqus_alt.ma".
-include "basic_2/multiple/lleq_ldrop.ma".
+include "basic_2/multiple/lleq_drop.ma".
(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2.
#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H //
- #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
+ #K1 #H1 #H2 lapply (drop_inv_O2 … H1) -H1
#H destruct /2 width=3 by fqu_lref_O, ex2_intro/
| * [ #a ] #I #G #L2 #V #T #L1 #H
[ elim (lleq_inv_bind … H)
| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
/2 width=3 by fqu_flat_dx, ex2_intro/
| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
- elim (ldrop_O1_le (Ⓕ) (e+1) L1)
+ elim (drop_O1_le (Ⓕ) (e+1) L1)
[ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
- | lapply (ldrop_fwd_length_le2 … HLK2) -K2
+ | lapply (drop_fwd_length_le2 … HLK2) -K2
lapply (lleq_fwd_length … HL12) -T -U //
]
]