include "ground_2/ynat/ynat_plus.ma".
include "basic_2/notation/relations/freestar_4.ma".
include "basic_2/substitution/lift_neg.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/substitution/drop.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
lemma frees_inv_lref_free: āL,d,j,i. L ā¢ i Ļµ š
*[d]ā¦#jā¦ ā |L| ā¤ j ā j = i.
#L #d #j #i #H #Hj elim (frees_inv_lref ā¦ H) -H //
-* #I #K #W #_ #_ #HLK lapply (ldrop_fwd_length_lt2 ā¦ HLK) -I
+* #I #K #W #_ #_ #HLK lapply (drop_fwd_length_lt2 ā¦ HLK) -I
#H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/
qed-.
| * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_bind ā¦ HnX) -HnX
[ /4 width=9 by frees_be, or_introl/
| #HnT @or_intror @(frees_be ā¦ HnT) -HnT
- [4,5,6: /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/
+ [4,5,6: /2 width=1 by drop_drop, yle_succ, lt_minus_to_plus/
|7: >minus_plus_plus_l //
|*: skip
]
elim (yle_inv_succ1 ā¦ Hdj) -Hdj <yminus_SO2 #Hyj #H
lapply (ylt_O ā¦ H) -H #Hj
>(plus_minus_m_m j 1) in HnU; // <minus_le_minus_minus_comm in HW;
- /4 width=9 by frees_be, nlift_bind_dx, ldrop_inv_drop1_lt, lt_plus_to_minus/
+ /4 width=9 by frees_be, nlift_bind_dx, drop_inv_drop1_lt, lt_plus_to_minus/
]
qed.