∀ {α : Type u_1} [inst : BEq α] {i l acc p s : List α},
  List.dropInfix?.go i l acc = some (p, s) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', l = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length