{ assumption }
case if_false.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hst : (T, s) ⟹ t
ih : RTC SmallStep (T, s) (Stmt.skip, t)
⊢ RTC SmallStep (T, s) (Stmt.skip, t)
no goals