Stuck on the proof of a simple Lemma: which induction should I use?

Question

I have the following structures:

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

Definition prog := list instr.

and the following function:

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.

Now I'd like to prove this simple Lemma:


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')

Note: As mentioned in the answer bellow, the more general form of the lemma is false:


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')

Whatever induction principle I use, I'm stuck.

For example, I've tried this induction pattern:

A: Type

forall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)) -> forall l : list A, P l
A: Type

forall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)) -> forall l : list A, P l
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)

forall l : list A, P l
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l

forall l : list A, P l
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l

P nil
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list A
P (x :: l)
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l

P nil
exact Pn.
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list A

P (x :: l)
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
l: list A

P l -> P (x :: l)
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
Pl: P nil

P (x :: nil)
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)
P (x :: y :: tl)
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x: A
Pl: P nil

P (x :: nil)
exact (P1 x).
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)

P (x :: y :: tl)
A: Type
P: list A -> Prop
Pn: P nil
P1: forall a : A, P (a :: nil)
Prec: forall (a b : A) (tl : list A), P tl -> P (a :: b :: tl)
tsli: forall l : list A, P l
x, y: A
tl: list A
Pl: P (y :: tl)

P tl
exact (tsli tl). Defined.

But I didn't manage to finalize the proof. There must be something obvious I don't see. Can't someone help me with this proof?

Answer

There are two problems with your question. The first one is that the statement you want to prove is false, here is a proof of a counter example.


~ (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'))

~ (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'))
abs: 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')

False
abs: 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')
tmp: Forward ((1 :: 2 :: nil) ++ 1 :: 2 :: nil) (nil ++ 1 :: 2 :: nil) = Some ((Select 1 :: Backspace :: nil) ++ Select 1 :: Select 2 :: nil)

False
abs: 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')
tmp: Some (Select 1 :: Select 2 :: Select 1 :: Backspace :: nil) = Some (Select 1 :: Backspace :: Select 1 :: Select 2 :: nil)

False
discriminate. Qed.

So, contrary to your claim, this is not a simple lemma.

The second problem is that the function has a complicated shape and the proof by induction is difficult to organize. I cover this aspect just below.

From the structure of the function Forward, it is natural that you should perform your proof by induction over the input argument, because it is the argument where recursive calls occur on a subterm. However the proof is made complicated by the fact that recursive calls happen not only on direct subterms (as in Forward rest ...) but also in subterms of subterms (as in Forward rrest ...).

There are several ways out of this difficulty, but all require some amount of explanation or learning.

  1. One way is to use the Equations plugin to Coq and redefine your Forward function using Equations. You can then use functional induction to solve your problem: this will use an induction principle that especially tailored to your problem.

  2. A second way is to build a tailored induction principle by hand. Here is an attempt.

    A: Type

    forall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)) -> forall l : list A, P l
    A: Type

    forall P : list A -> Prop, P nil -> (forall a : A, P (a :: nil)) -> (forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)) -> forall l : list A, P l
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)

    forall l : list A, P l
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l

    forall l : list A, P l
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l

    P nil
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x: A
    l: list A
    P (x :: l)
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l

    P nil
    exact Pn.
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x: A
    l: list A

    P (x :: l)
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x: A
    l: list A

    P l -> P (x :: l)
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x: A
    Pl: P nil

    P (x :: nil)
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x, y: A
    tl: list A
    Pl: P (y :: tl)
    P (x :: y :: tl)
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x: A
    Pl: P nil

    P (x :: nil)
    exact (P1 x).
    A: Type
    P: list A -> Prop
    Pn: P nil
    P1: forall a : A, P (a :: nil)
    Prec: forall (a b : A) (tl : list A), P (b :: tl) -> P tl -> P (a :: b :: tl)
    tsli: forall l : list A, P l
    x, y: A
    tl: list A
    Pl: P (y :: tl)

    P (x :: y :: tl)
    apply Prec; [assumption | exact (tsli tl)]. Defined.

    You can then start your proof with a command of the following shape:


    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')

    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')
    p, p': prog
    input1: list nat

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

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

    forall (p : prog) (input2 output1 output2 : list nat), Forward nil output1 = Some p -> Forward input2 output2 = Some p' -> Forward (nil ++ input2) (output1 ++ output2) = Some (p ++ p')
    p': prog
    a: nat
    forall (p : prog) (input2 output1 output2 : list nat), Forward (a :: nil) output1 = Some p -> Forward input2 output2 = Some p' -> Forward ((a :: nil) ++ input2) (output1 ++ output2) = Some (p ++ p')
    p': prog
    a, b: nat
    tl: list nat
    Ih1: forall (p : prog) (input2 output1 output2 : list nat), Forward (b :: tl) output1 = Some p -> Forward input2 output2 = Some p' -> Forward ((b :: tl) ++ input2) (output1 ++ output2) = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output1 output2 : list nat), Forward tl output1 = Some p -> Forward input2 output2 = Some p' -> Forward (tl ++ input2) (output1 ++ output2) = Some (p ++ p')
    forall (p : prog) (input2 output1 output2 : list nat), Forward (a :: b :: tl) output1 = Some p -> Forward input2 output2 = Some p' -> Forward ((a :: b :: tl) ++ input2) (output1 ++ output2) = Some (p ++ p')

    But, as I already said, the lemma you want to prove is actually false, so there is no way this proof will ever work and I cannot illustrate that the proposed approach is going to work.

    EDIT: Now that the original question has been corrected, here is a full correction to the original question:


    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')

    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')
    p, p': prog
    input1: list nat

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

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

    forall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')
    p': prog
    x: nat
    forall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog

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

    forall (p : prog) (input2 output : list nat), match output with | nil => Some nil | _ :: _ => None end = Some p -> Forward input2 nil = Some p' -> Forward input2 output = Some (p ++ p')
    p', p: prog
    input2: list nat

    Some nil = Some p -> Forward input2 nil = Some p' -> Forward input2 nil = Some (p ++ p')
    p', p: prog
    input2: list nat
    no1: nat
    output: list nat
    None = Some p -> Forward input2 nil = Some p' -> Forward input2 (no1 :: output) = Some (p ++ p')
    p', p: prog
    input2: list nat

    Some nil = Some p -> Forward input2 nil = Some p' -> Forward input2 nil = Some (p ++ p')
    p', p: prog
    input2: list nat
    p_is_nil: nil = p

    Forward input2 nil = Some p' -> Forward input2 nil = Some (p ++ p')
    p', p: prog
    input2: list nat
    p_is_nil: nil = p

    Forward input2 nil = Some p' -> Forward input2 nil = Some (nil ++ p')
    p', p: prog
    input2: list nat
    p_is_nil: nil = p

    Forward input2 nil = Some p' -> Forward input2 nil = Some p'
    auto.
    p', p: prog
    input2: list nat
    no1: nat
    output: list nat

    None = Some p -> Forward input2 nil = Some p' -> Forward input2 (no1 :: output) = Some (p ++ p')
    discriminate.
    p': prog
    x: nat

    forall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')
    p': prog
    x: nat

    forall (p : prog) (input2 output : list nat), match output with | nil => None | y :: r => if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None end = Some p -> Forward input2 nil = Some p' -> match output with | nil => match input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end | y :: r => if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest output with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end end = Some (p ++ p')
    p': prog
    x: nat
    p: prog
    input2: list nat
    y: nat
    r: list nat

    (if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None) = Some p -> Forward input2 nil = Some p' -> (if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end) = Some (p ++ p')
    p': prog
    x: nat
    p: prog
    input2: list nat
    y: nat
    r: list nat

    match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')
    p': prog
    x: nat
    p: prog
    input2: list nat
    y: nat

    Some (Select x :: nil) = Some p -> Forward input2 nil = Some p' -> match Forward input2 nil with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')
    now intros [= pval] v2; rewrite <- pval, v2; simpl.
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat

    Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat

    Forward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    Forward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat

    Forward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat

    match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    v: prog
    vtl: Forward rrest nil = Some v

    Some (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'
    tmp: Forward (rrest ++ input2) nil = Some (v ++ p')

    Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'
    tmp: Forward (rrest ++ input2) nil = Some (v ++ p')

    match Forward (rrest ++ input2) nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'
    tmp: Forward (rrest ++ input2) nil = Some (v ++ p')

    Some (Select x :: Backspace :: v ++ p') = Some ((Select x :: Backspace :: v) ++ p')
    easy.
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat

    Forward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat

    (if x =? y then match Forward (xx :: rrest) r with | Some pp => Some (Select x :: pp) | None => None end else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest

    (if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    (if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest

    (if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true

    Some (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true

    Some (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    vp: Select x :: vrest = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    vp: Select x :: vrest = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    Forward ((xx :: rrest) ++ input2) r = Some (vrest ++ p') -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: vrest ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'
    it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')

    match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'
    it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')

    Some (Select x :: vrest ++ p') = Some (Select x :: vrest ++ p')
    easy.
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false

    match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v

    Some (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')
    easy.
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None

    (if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false

    match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v

    Some (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')
    p': prog
    x, xx: nat
    rrest: list nat
    Ih1: forall (p : prog) (input2 output : list nat), Forward (xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((xx :: rrest) ++ input2) output = Some (p ++ p')
    Ih2: forall (p : prog) (input2 output : list nat), Forward rrest output = Some p -> Forward input2 nil = Some p' -> Forward (rrest ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')
    easy. Qed.

    A few comments on this solution:

    • The code posted in the original function contains 3 recursive calls, one where the argument is the immediate sublist (rest) and 2 where the argument is the second sublist (rest). The first one is handled by induction hypothesis Ih1 and the other are handled by induction hypothesis Ih2. For a reason I have no time to investigate, my proof needs 4 uses of induction hypotheses instead of 3. This means that there is probably some duplication.

    • Sometimes, the simpl tactic is too eager to unroll the recursive definition until it can no longer do anything. To counterbalance this bias of the simpl tactic, I had to perform one of the unrolling steps by hand, without relying on simpl. This unrolling step is performed by the change tactic call that appears in the middle of the script.

    • Everytime that there is a recursive call in your function, the result is later analyzed by a match construct. To account for this, the proof perform case analysis on the results of recursive calls and uses the destruct ... eqn:... variant of the destruct tactic to perform this analysis.

    • Aside from these advanced techniques, the proof is just guided by the interaction with Coq.

    This proof script was verified with coq-8.15 with the List and ZArith modules imported.

  3. You can avoid constructing a tailored induction principle by relying on much more powerful well founded induction. This will give you a more general induction hypothesis, which can be used for a much wider set of recursive arguments (even arguments that are not structural subterms of the initial first list). Here is the full script:

    Require Import Wellfounded.
    
    

    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')

    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')
    p, p': prog
    input1: list nat

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

    forall (p : prog) (input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    Ih: forall y : list nat, length y < length input1 -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), Forward input1 output = Some p -> Forward input2 nil = Some p' -> Forward (input1 ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x: nat
    input1eq: input1 = x :: nil
    Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    forall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), Forward nil output = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat

    Forward nil nil = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    no1: nat
    output: list nat
    Forward nil (no1 :: output) = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) (no1 :: output) = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat

    Forward nil nil = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    p_is_nil: nil = p

    Forward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    p_is_nil: nil = p

    Forward input2 nil = Some p' -> Forward (nil ++ input2) nil = Some (nil ++ p')
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    p_is_nil: nil = p

    Forward input2 nil = Some p' -> Forward input2 nil = Some p'
    auto.
    p': prog
    input1: list nat
    input1eq: input1 = nil
    Ih: forall y : list nat, length y < length nil -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    no1: nat
    output: list nat

    Forward nil (no1 :: output) = Some p -> Forward input2 nil = Some p' -> Forward (nil ++ input2) (no1 :: output) = Some (p ++ p')
    discriminate.
    p': prog
    input1: list nat
    x: nat
    input1eq: input1 = x :: nil
    Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), Forward (x :: nil) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: nil) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x: nat
    input1eq: input1 = x :: nil
    Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), match output with | nil => None | y :: r => if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None end = Some p -> Forward input2 nil = Some p' -> match output with | nil => match input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end | y :: r => if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest output with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end end = Some (p ++ p')
    p': prog
    input1: list nat
    x: nat
    input1eq: input1 = x :: nil
    Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat

    (if x =? y then match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end else None) = Some p -> Forward input2 nil = Some p' -> (if x =? y then match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end else match input2 with | nil => None | _ :: rrest => match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end end) = Some (p ++ p')
    p': prog
    input1: list nat
    x: nat
    input1eq: input1 = x :: nil
    Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat

    match match r with | nil => Some nil | _ :: _ => None end with | Some pp => Some (Select x :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> match Forward input2 r with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')
    p': prog
    input1: list nat
    x: nat
    input1eq: input1 = x :: nil
    Ih: forall y : list nat, length y < length (x :: nil) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat

    Some (Select x :: nil) = Some p -> Forward input2 nil = Some p' -> match Forward input2 nil with | Some pp => Some (Select x :: pp) | None => None end = Some (p ++ p')
    now intros [= pval] v2; rewrite <- pval, v2; simpl.
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')

    forall (p : prog) (input2 output : list nat), Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat

    Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat

    length rrest < length (x :: xx :: rrest)
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat

    length rrest < length (x :: xx :: rrest)
    now simpl; auto with arith.
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)

    Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)

    length (xx :: rrest) < length (x :: xx :: rrest)
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)

    length (xx :: rrest) < length (x :: xx :: rrest)
    now simpl; auto with arith.
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2, output: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)

    Forward (x :: xx :: rrest) output = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) output = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)

    Forward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    Forward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)

    Forward (x :: xx :: rrest) nil = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)

    match Forward rrest nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    v: prog
    vtl: Forward rrest nil = Some v

    Some (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'
    tmp: Forward (rrest ++ input2) nil = Some (v ++ p')

    Forward ((x :: xx :: rrest) ++ input2) nil = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'
    tmp: Forward (rrest ++ input2) nil = Some (v ++ p')

    match Forward (rrest ++ input2) nil with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    v: prog
    vtl: Forward rrest nil = Some v
    pval: Select x :: Backspace :: v = p
    p'val: Forward input2 nil = Some p'
    tmp: Forward (rrest ++ input2) nil = Some (v ++ p')

    Some (Select x :: Backspace :: v ++ p') = Some ((Select x :: Backspace :: v) ++ p')
    easy.
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)

    Forward (x :: xx :: rrest) (y :: r) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)

    (if x =? y then match Forward (xx :: rrest) r with | Some pp => Some (Select x :: pp) | None => None end else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest

    (if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    (if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest

    (if x =? y then Some (Select x :: vrest) else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true

    Some (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true

    Some (Select x :: vrest) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    vp: Select x :: vrest = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    vp: Select x :: vrest = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    Forward ((xx :: rrest) ++ input2) r = Some (vrest ++ p') -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: vrest) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: vrest ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'

    match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p') -> match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'
    it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')

    match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end = Some (Select x :: vrest ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = true
    v2: Forward input2 nil = Some p'
    it: match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end = Some (vrest ++ p')

    Some (Select x :: vrest ++ p') = Some (Select x :: vrest ++ p')
    easy.
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false

    match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v

    Some (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    vrest: prog
    eqnrest: Forward (xx :: rrest) r = Some vrest
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')
    easy.
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None

    (if x =? y then None else match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false

    match Forward rrest (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v

    Some (Select x :: Backspace :: v) = Some p -> Forward input2 nil = Some p' -> Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some (p ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    vp: Select x :: Backspace :: v = p
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Forward ((x :: xx :: rrest) ++ input2) (y :: r) = Some ((Select x :: Backspace :: v) ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    (if x =? y then match match r with | nil => match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest nil with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end | y :: r0 => if xx =? y then match Forward (rrest ++ input2) r0 with | Some pp => Some (Select xx :: pp) | None => None end else match rrest ++ input2 with | nil => None | _ :: rrest => match Forward rrest r with | Some pp => Some (Select xx :: Backspace :: pp) | None => None end end end with | Some pp => Some (Select x :: pp) | None => None end else match Forward (rrest ++ input2) (y :: r) with | Some pp => Some (Select x :: Backspace :: pp) | None => None end) = Some (Select x :: Backspace :: v ++ p')
    p': prog
    input1: list nat
    x, xx: nat
    rrest: list nat
    input1eq: input1 = x :: xx :: rrest
    Ih: forall y : list nat, length y < length (x :: xx :: rrest) -> forall (p : prog) (input2 output : list nat), Forward y output = Some p -> Forward input2 nil = Some p' -> Forward (y ++ input2) output = Some (p ++ p')
    p: prog
    input2: list nat
    y: nat
    r: list nat
    rrestlt: length rrest < length (x :: xx :: rrest)
    restlt: length (xx :: rrest) < length (x :: xx :: rrest)
    eqnrest: Forward (xx :: rrest) r = None
    xeqy: (x =? y) = false
    v: prog
    eqnrrest: Forward rrest (y :: r) = Some v
    v2: Forward input2 nil = Some p'

    Some (Select x :: Backspace :: v ++ p') = Some (Select x :: Backspace :: v ++ p')
    easy. Qed.

    A careful scrutiny of the script for lemma app_forward2 shows that the script is almost the same as for app_forward. Three main hints:

    • well_founded_induction combined with wf_inverse_image, length and lt_wf gives a general induction hypothesis that can be use for every case where input1 is replaced with a list that is shorter in length.

    • destruct input1 replaces every instance of input1 with a variety of cases, including the instance that appears in the induction hypothesis.

    • all calls to induction hypotheses Ih1 and Ih2 in the previous solution have simply been replaced by calls to Ih, using hypotheses restlt and rrestlt to guarantee length decrease.