simp only [disEval, List.mem_map, exists_exists_and_eq_and, unfoldBox, disconEval]
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset α ℓ φ)) (allTP α))) ↔ evaluate M w (discon (unfoldBox α φ))
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) ↔ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f