-include "Basic_2/substitution/ldrop.ma".
-include "Basic_2/unfold/gr2_minus.ma".
-include "Basic_2/unfold/lifts.ma".
+include "basic_2/substitution/ldrop.ma".
+include "basic_2/unfold/gr2_minus.ma".
+include "basic_2/unfold/lifts.ma".
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
inductive ldrops: list2 nat nat → relation lenv ≝
| ldrops_nil : ∀L. ldrops ⟠ L L
| ldrops_cons: ∀L1,L,L2,des,d,e.
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
inductive ldrops: list2 nat nat → relation lenv ≝
| ldrops_nil : ∀L. ldrops ⟠ L L
| ldrops_cons: ∀L1,L,L2,des,d,e.
- ∀d,e,tl. des = {d, e} :: tl →
+ ∀d,e,tl. des = {d, e} @ tl →
∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2.
#L1 #L2 #des * -L1 -L2 -des
[ #L #d #e #tl #H destruct
∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2.
#L1 #L2 #des * -L1 -L2 -des
[ #L #d #e #tl #H destruct
-lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 →
+lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 →