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]
case cons
t : Prop
l : List Prop
ih : ∀ {ps : List Prop} {i j : Nat}, orN ps → ps = drop i (take j l) → orN l
ps : List Prop
i j : Nat
hp : orN ps
hps : ps = drop i (take j (t :: l))
⊢ t ∨ orN l
no goals