case op.op ih _ _ => simpa [encodeProgram] using λ x y ↦ ⟨x, ih y⟩
inst✝¹ : OpInstruction
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.op inst✝ next✝
no goals