{ apply SmallStep.if_true
  assumption }
case if_true.hab
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ (Stmt.ifThenElse B S T, s) ⇒ ?if_true.b

case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep ?if_true.b (Stmt.skip, t)

case if_true.b
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ Stmt × State
case if_true.hbc
Ss : Stmt × State
t✝ : State
B : State → Prop
S T : Stmt
s t : State
hB : B s
hst : (S, s) ⟹ t
ih : RTC SmallStep (S, s) (Stmt.skip, t)
⊢ RTC SmallStep (S, s) (Stmt.skip, t)