aesop
case while_true.while_false
Ss : Stmt × State
l✝ : State
B : State → Prop
S : Stmt
s l₀ l : State
hB : B s
hS : (S, s) ⟹ l₀
hw : (Stmt.whileDo B S, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihw : ∀ {r : State}, (Stmt.whileDo B S, l₀) ⟹ r → l = r
hB' : ¬B s
⊢ l = s
no goals