cases hr with
| if_true _ _ _ _ _ hB' hS'  => apply ih hS'
| if_false _ _ _ _ _ hB' hS' => aesop
case if_true
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : B s
hS : (S, s) ⟹ l
ih : ∀ {r : State}, (S, s) ⟹ r → l = r
r : State
hr : (Stmt.ifThenElse B S T, s) ⟹ r
⊢ l = r
no goals