induction hl generalizing Rr with
| assign x a s =>
  cases hr with
  | assign _ _ _ => rfl
| seq_step S S₁ T s s₁ hS₁ ih =>
  cases hr with
  | seq_step S S₂ _ _ s₂ hS₂ =>
    have hSs₁₂ :=
      ih hS₂
    aesop
  | seq_skip => cases hS₁
| seq_skip T s =>
  cases hr with
  | seq_step _ S _ _ s' hskip => cases hskip
  | seq_skip                  => rfl
| if_true B S T s hB =>
  cases hr with
  | if_true  => rfl
  | if_false => aesop
| if_false B S T s hB =>
  cases hr with
  | if_true  => aesop
  | if_false => rfl
| whileDo B S s =>
  cases hr with
  | whileDo => rfl
Ss Ll Rr : Stmt × State
hl : Ss ⇒ Ll
hr : Ss ⇒ Rr
⊢ Ll = Rr
no goals