Coq中Forward函数的app_forward引理证明：如何选择归纳法？

我定义了如下类型与程序结构：

Inductive instr : Set :=
 | Select    : nat -> instr
 | Backspace : instr.

Definition prog := list instr.

以及如下Forward函数：

Fixpoint Forward (input output: list nat) : option prog :=
match input with
  | nil => match output with
                 | nil => Some nil
                 | y::r => None
           end
  | x::rest => match output with
                | nil => match rest with
                            | nil => None   
                            | xx::rrest => match (Forward rrest nil) with
                                                            | Some pp => Some ((Select x) :: Backspace :: pp)
                                                            | None => None
                                           end
                         end
                | y::r => if ( beq_nat x y ) then match (Forward rest r) with
                                                   | Some pp => Some ((Select x) :: pp)
                                                   | None => None 
                                                   end
                          else match rest with
                                             | nil => None
                                             | xx::rrest => match (Forward rrest output) with
                                                                           | Some pp => Some ((Select x) :: Backspace :: pp)
                                                                           | None => None                                                                          
                                                            end
                                end

                end
end.

我希望证明如下引理：

Lemma app_forward :
  forall (p p':prog) (input1 input2 output:list nat),
    Forward input1 output = Some p ->
        Forward input2 nil = Some p' ->
           Forward (input1 ++ input2) output = Some (p++p').

注：如下更通用形式的引理并不成立：

Lemma not_app_forward :
  forall (p p':prog) (input1 input2 output1 output2:list nat),
    Forward input1 output1 = Some p ->
        Forward input2 output2 = Some p' ->
           Forward (input1 ++ input2) (output1 ++ output2) = Some (p++p').

我尝试过多种归纳原理，比如自定义了如下归纳模式：

Definition list_pair_induction {A : Type} :
  forall (P : list A -> Prop),
    P nil ->
    (forall a, P (a :: nil)) ->
    (forall a b tl, P tl -> P (a :: b :: tl)) ->
  forall l, P l.
Proof.
intros P Pn P1 Prec.
fix tsli 1.
intros [ | x l].
  exact Pn.
  generalize (tsli l).
destruct l as [ | y tl]; intros Pl.
    exact (P1 x).
  apply Prec. exact (tsli tl).
Defined.

但始终无法完成证明，肯定是忽略了某些关键点，求帮忙完成这个证明。

内容的提问来源于stack exchange，提问作者FH35