Theorem: starIffFinitelyManyStepsModel (Pdl/Examples.lean)

State before:
W : Type
M : KripkeModel W
x z : W
α : Program
⊢ Relation.ReflTransGen (relate M α) x z ↔
    ∃ n ys, x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), relate M α (ys.get i.castSucc) (ys.get i.succ)
Tactic:
exact ReflTransGen.iff_finitelyManySteps (relate M α) x z
State after:
no goals