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