G ⊢ ~⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⬊*[h, g, V, ⫰(d-i)] K.
#h #g #G #L #d #H elim H -L -d
[ #d #J #K #V #i #H elim (drop_inv_atom1 … H) -H #H destruct
G ⊢ ~⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⬊*[h, g, V, ⫰(d-i)] K.
#h #g #G #L #d #H elim H -L -d
[ #d #J #K #V #i #H elim (drop_inv_atom1 … H) -H #H destruct