case test τ =>
  simp [evaluate, H, Yset]
  rw [conEval]
  simp
ψ : Formula
W : Type
M : KripkeModel W
w : W
τ : Formula
⊢ evaluate M w (~⌈?'τ⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (?'τ))))
no goals