āi,L. ā¬*[i] L ā” K ā L ā¢ š
*ā¦#(i+j)ā¦ ā” ā*[i] f.
#f #K #j #Hf #i elim i -i
[ #L #H lapply (drops_fwd_isid ā¦ H ?) -H //
-| #i #IH #L #H elim (drops_inv_succ ā¦ H) -H /3 width=1 by frees_lref/
+| #i #IH #L #H elim (drops_inv_succ ā¦ H) -H
+ #I #Y #V #HYK #H destruct /3 width=1 by frees_lref/
]
qed.