apply SmallStep.whileDo
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ (Stmt.whileDo B S, s) ⇒ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s)
no goals