intro v
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
⊢ ∀ (v : W), relate M a w v → evaluate M v X
case left
a : Program
X Y : Formula
W : Type
M : KripkeModel W
w : W
hyp : ∀ (v : W), relate M a w v → evaluate M v X ∧ evaluate M v Y
v : W
⊢ relate M a w v → evaluate M v X