apply ih hS'
case if_false.if_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S T : Stmt
s l : State
hB : ¬B s
hT : (T, s) ⟹ l
ih : ∀ {r : State}, (T, s) ⟹ r → l = r
r : State
hB' : ¬B s
hS' : (T, s) ⟹ r
⊢ l = r
no goals