Theorem: relateSeq_singelton (Pdl/Semantics.lean)

State before:
W : Type
M : KripkeModel W
α : Program
w v : W
⊢ relateSeq M [α] w v ↔ relate M α w v
Tactic:
simp [relateSeq]
State after:
no goals