apply Exists.intro t
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ ∃ t, (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u
case mp.loop_step.h
S : Stmt
s u t : State
hS : (S, s) ⟹ t
hl : (Stmt.loop S, t) ⟹ u
⊢ (S, s) ⟹ t ∧ (Stmt.loop S, t) ⟹ u