cases hr with
| seq _ _ _ r₀ _ hS' hT' =>
  cases ihS hS' with
  | refl =>
    cases ihT hT' with
    | refl => rfl
case seq
Ss : Stmt × State
l✝ : State
S T : Stmt
s l₀ l : State
hS : (S, s) ⟹ l₀
hT : (T, l₀) ⟹ l
ihS : ∀ {r : State}, (S, s) ⟹ r → l₀ = r
ihT : ∀ {r : State}, (T, l₀) ⟹ r → l = r
r : State
hr : (S; T, s) ⟹ r
⊢ l = r
no goals