ā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,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 //