done
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
w_1 : W
left : relate M α w w_1
right : ¬evaluate M w_1 φ
⊢ evaluate M w (discon (unfoldDiamond α φ))

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
a : evaluate M w (discon (unfoldDiamond α φ))
⊢ ∃ x, relate M α w x ∧ ¬evaluate M x φ
no goals