apply Iff.intro
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u ↔ s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
case mp
S : Stmt
s u : State
⊢ (Stmt.loop S, s) ⟹ u → s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u

case mpr
S : Stmt
s u : State
⊢ (s = u ∨ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u) → (Stmt.loop S, s) ⟹ u