exact w_a_v
case left.intro.left.h
a b : Program
X : Formula
W : Type
M : KripkeModel W
w : W
rhs : ¬False
v : W
lhs : relate M a w v ∨ relate M b w v → evaluate M v X
w_a_v : relate M a w v
⊢ relate M a w v
no goals