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.succ
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 : Nat
hp : orN ps
j : Nat
hps : ps = drop i (t :: take j l)
⊢ t ∨ orN l
no goals