(* Properties on append for local environments ******************************)
lemma frees_append: āL2,U,l,i. L2 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā i ā¤ |L2| ā
- āL1. L1 @@ L2 ā¢ i Ļµ š
*[l]ā¦Uā¦.
+ āL1. L1 ;; L2 ā¢ i Ļµ š
*[l]ā¦Uā¦.
#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1
lapply (drop_fwd_length_minus2 ā¦ HLK2) normalize #H0
(* Inversion lemmas on append for local environments ************************)
-fact frees_inv_append_aux: āL,U,l,i. L ā¢ i Ļµ š
*[l]ā¦Uā¦ ā āL1,L2. L = L1 @@ L2 ā
+fact frees_inv_append_aux: āL,U,l,i. L ā¢ i Ļµ š
*[l]ā¦Uā¦ ā āL1,L2. L = L1 ;; L2 ā
i ā¤ |L2| ā L2 ā¢ i Ļµ š
*[l]ā¦Uā¦.
#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/
#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct
]
qed-.
-lemma frees_inv_append: āL1,L2,U,l,i. L1 @@ L2 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā
+lemma frees_inv_append: āL1,L2,U,l,i. L1 ;; L2 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā
i ā¤ |L2| ā L2 ā¢ i Ļµ š
*[l]ā¦Uā¦.
/2 width=4 by frees_inv_append_aux/ qed-.