constructor
case left
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
⊢ evaluate M w X ∧ ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X
case left.left
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
⊢ evaluate M w X

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
⊢ ∀ (x : W), relate M a w x → ∀ (x_1 : W), Relation.ReflTransGen (relate M a) x x_1 → evaluate M x_1 X