simp [any, toPropFun, Clause.toPropFun]
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (any ls) ↔ τ ⊨ PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))
no goals