simp
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ (¬∃ T t, (Stmt.whileDo B S, s) ⇒ (T, t)) ↔ Stmt.whileDo B S = Stmt.skip
case whileDo
s : State
B : State → Prop
S : Stmt
ih : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
⊢ ∃ T t, (Stmt.whileDo B S, s) ⇒ (T, t)