apply starAX
case left.right
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ evaluate M v_1 X
case left.right.a
a : Program
X : Formula
W : Type
M : KripkeModel W
w : W
starAX : ∀ (v : W), Relation.ReflTransGen (relate M a) w v → evaluate M v X
v : W
w_a_v : relate M a w v
v_1 : W
v_aS_v1 : Relation.ReflTransGen (relate M a) v v_1
⊢ Relation.ReflTransGen (relate M a) w v_1