simp [*, orN] at *
case cons.zero
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
hps : ps = drop i (take 0 (t :: l))
⊢ t ∨ orN l
no goals