{ apply SmallStep.if_false
  assumption }
case if_false.hab
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)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_false.b

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 ?if_false.b (Stmt.skip, t)

case if_false.b
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)
⊢ Stmt × State
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)