apply ih hS'
case if_true.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
hB' : B s
hS' : (S, s) ⟹ r
⊢ l = r
no goals