induction qs with
| nil =>
  intro ps i j hp hps
  simp [subList', *] at *; assumption
| cons t l ih =>
  simp only [subList'] at *
  intro ps i j hp hps
  rw [orN_cons]
  cases j with
  | zero =>
    simp [*, orN] at *
  | succ j =>
    simp only [take_cons_succ] at hps
    cases i with
    | zero =>
      simp only [hps, orN_cons, drop_zero] at hp
      exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
    | succ i =>
      apply Or.inr
      apply @ih ps i j hp
      simp [hps]
qs : List Prop
⊢ ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = subList' qs i j → orN qs
no goals