(* Properties on append for local environments ******************************)
lemma frees_append: āL2,U,l,i. L2 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā i ā¤ |L2| ā
(* Properties on append for local environments ******************************)
lemma frees_append: āL2,U,l,i. L2 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā i ā¤ |L2| ā