#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
[ #HnX elim (nlift_inv_bind … HnX) -HnX
/4 width=2 by frees_eq, or_intror, or_introl/
| * #I #K #W #j #Hlj #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
#a #J #L #V #U #l #i #H elim (frees_inv … H) -H
[ #HnX elim (nlift_inv_bind … HnX) -HnX
/4 width=2 by frees_eq, or_intror, or_introl/
| * #I #K #W #j #Hlj #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