case dia α φ =>
  rw [conEval]
  simp only [List.mem_singleton, forall_eq, discon, unfoldDiamond]
  rw [localDiamondTruth α φ W M w, disEval, disconEval]
  apply mapCon_mapForall
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ evaluate M w (Con [~⌈α⌉φ]) ↔ evaluate M w (discon (unfoldDiamond α φ))
no goals