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