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
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