induction hl generalizing r with
| skip s =>
  cases hr with
  | skip => rfl
| assign x a s =>
  cases hr with
  | assign => rfl
| seq S T s l₀ l hS hT ihS ihT =>
  cases hr with
  | seq _ _ _ r₀ _ hS' hT' =>
    cases ihS hS' with
    | refl =>
      cases ihT hT' with
      | refl => rfl
| if_true B S T s l hB hS ih =>
  cases hr with
  | if_true _ _ _ _ _ hB' hS'  => apply ih hS'
  | if_false _ _ _ _ _ hB' hS' => aesop
| if_false B S T s l hB hT ih =>
  cases hr with
  | if_true _ _ _ _ _ hB' hS'  => aesop
  | if_false _ _ _ _ _ hB' hS' => apply ih hS'
| while_true B S s l₀ l hB hS hw ihS ihw =>
  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
| while_false B S s hB =>
  cases hr with
  | while_true _ _ _ s' _ hB' hS hw => aesop
  | while_false _ _ _ hB'           => rfl
Ss : Stmt × State
l r : State
hl : Ss ⟹ l
hr : Ss ⟹ r
⊢ l = r
no goals