simpa [encodeProgram] using λ hop hf ht ↦
  ⟨ hop, funext λ | false => nih _ hf | true => nih _ ht ⟩
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
nih : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.branch inst✝ next✝
no goals