cases ihS hS' with
| refl =>
  cases ihT hT' with
  | refl => rfl
case seq.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 r₀ : State
hS' : (S, s) ⟹ r₀
hT' : (T, r₀) ⟹ r
⊢ l = r
no goals