exact Relation.ReflTransGen.refl
case left.left.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
⊢ Relation.ReflTransGen (relate M a) w w
no goals