Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
case exit.exit

⊢ encodeProgram Program.exit = encodeProgram Program.exit → Program.exit = Program.exit

case exit.op
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.op inst✝ next✝) → Program.exit = Program.op inst✝ next✝

case exit.branch
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram Program.exit = encodeProgram (Program.branch inst✝ next✝) → Program.exit = Program.branch inst✝ next✝

case exit.subroutine
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.exit = Program.subroutine dst✝ src✝ func✝ next✝

case exit.recurse
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.exit = Program.recurse dst✝ src✝ next✝

case op.exit
inst✝ : OpInstruction
next✝ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.op inst✝ next✝) = encodeProgram Program.exit → Program.op inst✝ next✝ = Program.exit

case op.branch
inst✝¹ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.branch inst✝ next✝

case op.subroutine
inst✝ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.op inst✝ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.op inst✝ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case op.recurse
inst✝ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.op inst✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.op inst✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case branch.exit
inst✝ : BranchInstruction
next✝ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝ a) = encodeProgram p₁ → next✝ a = p₁
⊢ encodeProgram (Program.branch inst✝ next✝) = encodeProgram Program.exit → Program.branch inst✝ next✝ = Program.exit

case branch.op
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.op inst✝ next✝

case branch.subroutine
inst✝ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.branch inst✝ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.branch inst✝ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case branch.recurse
inst✝ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.branch inst✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.branch inst✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case subroutine.exit
dst✝ src✝ : Source
func✝ next✝ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) = encodeProgram Program.exit →
    Program.subroutine dst✝ src✝ func✝ next✝ = Program.exit

case subroutine.op
dst✝ src✝ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.subroutine dst✝ src✝ func✝ next✝¹ = Program.op inst✝ next✝

case subroutine.branch
dst✝ src✝ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.subroutine dst✝ src✝ func✝ next✝¹ = Program.branch inst✝ next✝

case subroutine.recurse
dst✝¹ src✝¹ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case recurse.exit
dst✝ src✝ : Source
next✝ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝) = encodeProgram Program.exit →
    Program.recurse dst✝ src✝ next✝ = Program.exit

case recurse.op
dst✝ src✝ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.recurse dst✝ src✝ next✝¹ = Program.op inst✝ next✝

case recurse.branch
dst✝ src✝ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.recurse dst✝ src✝ next✝¹ = Program.branch inst✝ next✝

case recurse.subroutine
dst✝¹ src✝¹ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
all_goals simp [encodeProgram]
Proof state after:
no goals