cases hr with
| while_true _ _ _ r₀ hB' hB' hS' hw' =>
  cases ihS hS' with
  | refl =>
    cases ihw hw' with
    | refl => rfl
| while_false _ _ _ hB' => aesop
case while_true
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
r : State
hr : (Stmt.whileDo B S, s) ⟹ r
⊢ l = r
no goals