(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Fin.
Require Import VectorDef.
Import VectorNotations.

Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
 (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 :=
   match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1
   with | eq_refl => conj eq_refl eq_refl
   end.

Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v.
A:Type
n:nat
v:t A (S n)
v = hd v :: tl v
Proof.
A:Type
n:nat
v:t A (S n)
v = hd v :: tl v
intros; apply caseS with (v:=v); intros; reflexivity.
Defined.

Lemma eq_nth_iff A n (v1 v2: t A n):
  (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
A:Type
n:nat
v1, v2:t A n
(forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2]) <->
v1 = v2
Proof.
A:Type
n:nat
v1, v2:t A n
(forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2]) <->
v1 = v2
split.
A:Type
n:nat
v1, v2:t A n
(forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2]) ->
v1 = v2
A:Type
n:nat
v1, v2:t A n
v1 = v2 ->
forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2]
-
A:Type
n:nat
v1, v2:t A n
(forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2]) ->
v1 = v2 revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
A:Type
H:forall p1 p2 : Fin.t 0,
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n =>
    caseS (fun (n0 : nat) (_ : t A (S n0)) => A)
      (fun (h : A) (n0 : nat) (_ : t A n0) => h)
| @Fin.FS n p' =>
    fun v : t A (S n) =>
    caseS
      (fun (n0 : nat) (_ : t A (S n0)) =>
       Fin.t n0 -> A)
      (fun (_ : A) (n0 : nat) (t : t A n0)
         (p0 : Fin.t n0) => t[@p0]) v p'
end [] =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n =>
    caseS (fun (n0 : nat) (_ : t A (S n0)) => A)
      (fun (h : A) (n0 : nat) (_ : t A n0) => h)
| @Fin.FS n p' =>
    fun v : t A (S n) =>
    caseS
      (fun (n0 : nat) (_ : t A (S n0)) =>
       Fin.t n0 -> A)
      (fun (_ : A) (n0 : nat) (t : t A n0)
         (p0 : Fin.t n0) => t[@p0]) v p'
end []
[] = []
A:Type
n:nat
v1, v2:t A n
H:(forall p1 p2 : Fin.t n,
 p1 = p2 -> v1[@p1] = v2[@p2]) -> v1 = v2
a, b:A
H0:forall p1 p2 : Fin.t (S n),
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (a :: v1) =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (b :: v2)
a :: v1 = b :: v2
  +
A:Type
H:forall p1 p2 : Fin.t 0,
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n =>
    caseS (fun (n0 : nat) (_ : t A (S n0)) => A)
      (fun (h : A) (n0 : nat) (_ : t A n0) => h)
| @Fin.FS n p' =>
    fun v : t A (S n) =>
    caseS
      (fun (n0 : nat) (_ : t A (S n0)) =>
       Fin.t n0 -> A)
      (fun (_ : A) (n0 : nat) (t : t A n0)
         (p0 : Fin.t n0) => t[@p0]) v p'
end [] =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n =>
    caseS (fun (n0 : nat) (_ : t A (S n0)) => A)
      (fun (h : A) (n0 : nat) (_ : t A n0) => h)
| @Fin.FS n p' =>
    fun v : t A (S n) =>
    caseS
      (fun (n0 : nat) (_ : t A (S n0)) =>
       Fin.t n0 -> A)
      (fun (_ : A) (n0 : nat) (t : t A n0)
         (p0 : Fin.t n0) => t[@p0]) v p'
end []
[] = [] reflexivity.
  +
A:Type
n:nat
v1, v2:t A n
H:(forall p1 p2 : Fin.t n,
 p1 = p2 -> v1[@p1] = v2[@p2]) -> v1 = v2
a, b:A
H0:forall p1 p2 : Fin.t (S n),
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (a :: v1) =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (b :: v2)
a :: v1 = b :: v2 f_equal.
A:Type
n:nat
v1, v2:t A n
H:(forall p1 p2 : Fin.t n,
 p1 = p2 -> v1[@p1] = v2[@p2]) -> v1 = v2
a, b:A
H0:forall p1 p2 : Fin.t (S n),
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (a :: v1) =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (b :: v2)
a = b
A:Type
n:nat
v1, v2:t A n
H:(forall p1 p2 : Fin.t n,
 p1 = p2 -> v1[@p1] = v2[@p2]) -> v1 = v2
a, b:A
H0:forall p1 p2 : Fin.t (S n),
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (a :: v1) =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (b :: v2)
v1 = v2 apply (H0 Fin.F1 Fin.F1 eq_refl).
A:Type
n:nat
v1, v2:t A n
H:(forall p1 p2 : Fin.t n,
 p1 = p2 -> v1[@p1] = v2[@p2]) -> v1 = v2
a, b:A
H0:forall p1 p2 : Fin.t (S n),
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (a :: v1) =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (b :: v2)
v1 = v2
    apply H.
A:Type
n:nat
v1, v2:t A n
H:(forall p1 p2 : Fin.t n,
 p1 = p2 -> v1[@p1] = v2[@p2]) -> v1 = v2
a, b:A
H0:forall p1 p2 : Fin.t (S n),
p1 = p2 ->
match p1 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (a :: v1) =
match p2 in (Fin.t m') return (t A m' -> A) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
      (fun (h : A) (n1 : nat) (_ : t A n1) => h)
| @Fin.FS n0 p' =>
    fun v : t A (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t A (S n1)) =>
       Fin.t n1 -> A)
      (fun (_ : A) (n1 : nat) (t : t A n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (b :: v2)
forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2] intros p1 p2 H1;
    apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)).
-
A:Type
n:nat
v1, v2:t A n
v1 = v2 ->
forall p1 p2 : Fin.t n, p1 = p2 -> v1[@p1] = v2[@p2] intros; now f_equal.
Qed.

Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
 nth_order v H = last v.
A:Type
forall (n : nat) (v : t A (S n)) (H : n < S n),
nth_order v H = last v
Proof.
A:Type
forall (n : nat) (v : t A (S n)) (H : n < S n),
nth_order v H = last v
unfold nth_order; refine (@rectS _ _ _ _); now simpl.
Qed.

Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
  nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
A:Type
a:A
n:nat
v:t A n
k1, k2:Fin.t n
eq:k1 = k2
(shiftin a v)[@Fin.L_R 1 k1] = v[@k2]
Proof.
A:Type
a:A
n:nat
v:t A n
k1, k2:Fin.t n
eq:k1 = k2
(shiftin a v)[@Fin.L_R 1 k1] = v[@k2]
subst k2; induction k1.
A:Type
a:A
n:nat
v:t A (S n)
(shiftin a v)[@Fin.L_R 1 Fin.F1] = v[@Fin.F1]
A:Type
a:A
n:nat
v:t A (S n)
k1:Fin.t n
IHk1:forall v0 : t A n,
(shiftin a v0)[@Fin.L_R 1 k1] = v0[@k1]
(shiftin a v)[@Fin.L_R 1 (Fin.FS k1)] = v[@Fin.FS k1]
-
A:Type
a:A
n:nat
v:t A (S n)
(shiftin a v)[@Fin.L_R 1 Fin.F1] = v[@Fin.F1] generalize dependent n.
A:Type
a:A
forall (n : nat) (v : t A (S n)),
(shiftin a v)[@Fin.L_R 1 Fin.F1] = v[@Fin.F1] apply caseS ; intros.
A:Type
a, h:A
n:nat
t:VectorDef.t A n
(shiftin a (h :: t))[@Fin.L_R 1 Fin.F1] =
(h :: t)[@Fin.F1] now simpl.
-
A:Type
a:A
n:nat
v:t A (S n)
k1:Fin.t n
IHk1:forall v0 : t A n,
(shiftin a v0)[@Fin.L_R 1 k1] = v0[@k1]
(shiftin a v)[@Fin.L_R 1 (Fin.FS k1)] = v[@Fin.FS k1] generalize dependent n.
A:Type
a:A
forall (n : nat) (v : t A (S n)) (k1 : Fin.t n),
(forall v0 : t A n,
 (shiftin a v0)[@Fin.L_R 1 k1] = v0[@k1]) ->
(shiftin a v)[@Fin.L_R 1 (Fin.FS k1)] = v[@Fin.FS k1] refine (@caseS _ _ _) ; intros.
A:Type
a, h:A
n:nat
t:VectorDef.t A n
k1:Fin.t n
IHk1:forall v : VectorDef.t A n,
(shiftin a v)[@Fin.L_R 1 k1] = v[@k1]
(shiftin a (h :: t))[@Fin.L_R 1 (Fin.FS k1)] =
(h :: t)[@Fin.FS k1] now simpl.
Qed.

Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a.
A:Type
a:A
n:nat
v:t A n
last (shiftin a v) = a
Proof.
A:Type
a:A
n:nat
v:t A n
last (shiftin a v) = a
induction v ;now simpl.
Qed.

Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
  nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
A:Type
forall (n : nat) (k : Fin.t (S n)) (v : t A (S n)),
(shiftrepeat v)[@Fin.L_R 1 k] = v[@k]
Proof.
A:Type
forall (n : nat) (k : Fin.t (S n)) (v : t A (S n)),
(shiftrepeat v)[@Fin.L_R 1 k] = v[@k]
refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
A:Type
n:nat
v:t A (S n)
(shiftrepeat v)[@Fin.L_R 1 Fin.F1] = v[@Fin.F1]
A:Type
n:nat
p:Fin.t (S n)
H:forall v0 : t A (S n),
(shiftrepeat v0)[@Fin.L_R 1 p] = v0[@p]
v:t A (S (S n))
(shiftrepeat v)[@Fin.L_R 1 (Fin.FS p)] = v[@Fin.FS p]
-
A:Type
n:nat
v:t A (S n)
(shiftrepeat v)[@Fin.L_R 1 Fin.F1] = v[@Fin.F1] revert n v; refine (@caseS _ _ _); simpl; intros.
A:Type
h:A
n:nat
t:VectorDef.t A n
(match
   n as n0
   return
     (VectorDef.t A n0 -> VectorDef.t A (S (S n0)))
 with
 | 0 =>
     fun v : VectorDef.t A 0 =>
     match
       v as v0 in (VectorDef.t _ n0)
       return
         (match
            n0 as x return (VectorDef.t A x -> Type)
          with
          | 0 =>
              fun _ : VectorDef.t A 0 =>
              VectorDef.t A 2
          | S n1 =>
              fun _ : VectorDef.t A (S n1) =>
              False -> IDProp
          end v0)
     with
     | [] => [h; h]
     | _ :: _ =>
         fun devil : False => False_ind IDProp devil
     end
 | S nn' =>
     fun v : VectorDef.t A (S nn') =>
     h :: shiftrepeat v
 end t)[@Fin.F1] = h now destruct t.
-
A:Type
n:nat
p:Fin.t (S n)
H:forall v0 : t A (S n),
(shiftrepeat v0)[@Fin.L_R 1 p] = v0[@p]
v:t A (S (S n))
(shiftrepeat v)[@Fin.L_R 1 (Fin.FS p)] = v[@Fin.FS p] revert p H.
A:Type
n:nat
v:t A (S (S n))
forall p : Fin.t (S n),
(forall v0 : t A (S n),
 (shiftrepeat v0)[@Fin.L_R 1 p] = v0[@p]) ->
(shiftrepeat v)[@Fin.L_R 1 (Fin.FS p)] = v[@Fin.FS p]
  refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
    |S (S n) => fun v => forall p : Fin.t (S n),
      (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
      (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
    |_ => fun _ => True end v' with
  |[] => I |h :: t => _ end).
A:Type
n:nat
v:VectorDef.t A (S (S n))
h:A
n0:nat
t:VectorDef.t A n0
match
  n0 as n1 return (VectorDef.t A (S n1) -> Prop)
with
| 0 => fun _ : VectorDef.t A 1 => True
| S n1 =>
    fun v0 : VectorDef.t A (S (S n1)) =>
    forall p : Fin.t (S n1),
    (forall v1 : VectorDef.t A (S n1),
     (shiftrepeat v1)[@Fin.L_R 1 p] = v1[@p]) ->
    (shiftrepeat v0)[@Fin.L_R 1 (Fin.FS p)] =
    v0[@Fin.FS p]
end (h :: t) destruct n0.
A:Type
n:nat
v:VectorDef.t A (S (S n))
h:A
t:VectorDef.t A 0
True
A:Type
n:nat
v:VectorDef.t A (S (S n))
h:A
n0:nat
t:VectorDef.t A (S n0)
forall p : Fin.t (S n0),
(forall v0 : VectorDef.t A (S n0),
 (shiftrepeat v0)[@Fin.L_R 1 p] = v0[@p]) ->
(shiftrepeat (h :: t))[@Fin.L_R 1 (Fin.FS p)] =
(h :: t)[@Fin.FS p] exact I.
A:Type
n:nat
v:VectorDef.t A (S (S n))
h:A
n0:nat
t:VectorDef.t A (S n0)
forall p : Fin.t (S n0),
(forall v0 : VectorDef.t A (S n0),
 (shiftrepeat v0)[@Fin.L_R 1 p] = v0[@p]) ->
(shiftrepeat (h :: t))[@Fin.L_R 1 (Fin.FS p)] =
(h :: t)[@Fin.FS p] now simpl.
Qed.

Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
A:Type
forall (n : nat) (v : t A (S n)),
last (shiftrepeat v) = last v
Proof.
A:Type
forall (n : nat) (v : t A (S n)),
last (shiftrepeat v) = last v
refine (@rectS _ _ _ _); now simpl.
Qed.

Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a.
A:Type
a:A
n:nat
p:Fin.t n
(const a n)[@p] = a
Proof.
A:Type
a:A
n:nat
p:Fin.t n
(const a n)[@p] = a
now induction p.
Qed.

Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2):
  (map f v) [@ p1] = f (v [@ p2]).
A, B:Type
f:A -> B
n:nat
v:t A n
p1, p2:Fin.t n
eq:p1 = p2
(map f v)[@p1] = f v[@p2]
Proof.
A, B:Type
f:A -> B
n:nat
v:t A n
p1, p2:Fin.t n
eq:p1 = p2
(map f v)[@p1] = f v[@p2]
subst p2; induction p1.
A, B:Type
f:A -> B
n:nat
v:t A (S n)
(map f v)[@Fin.F1] = f v[@Fin.F1]
A, B:Type
f:A -> B
n:nat
v:t A (S n)
p1:Fin.t n
IHp1:forall v0 : t A n, (map f v0)[@p1] = f v0[@p1]
(map f v)[@Fin.FS p1] = f v[@Fin.FS p1]
-
A, B:Type
f:A -> B
n:nat
v:t A (S n)
(map f v)[@Fin.F1] = f v[@Fin.F1] revert n v; refine (@caseS _ _ _); now simpl.
-
A, B:Type
f:A -> B
n:nat
v:t A (S n)
p1:Fin.t n
IHp1:forall v0 : t A n, (map f v0)[@p1] = f v0[@p1]
(map f v)[@Fin.FS p1] = f v[@Fin.FS p1] revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
Qed.

Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
  p1 = p2 -> p2 = p3 -> (map2 f v w) [@p1] = f (v[@p2]) (w[@p3]).
A, B, C:Type
f:A -> B -> C
n:nat
v:t A n
w:t B n
p1, p2, p3:Fin.t n
p1 = p2 ->
p2 = p3 -> (map2 f v w)[@p1] = f v[@p2] w[@p3]
Proof.
A, B, C:Type
f:A -> B -> C
n:nat
v:t A n
w:t B n
p1, p2, p3:Fin.t n
p1 = p2 ->
p2 = p3 -> (map2 f v w)[@p1] = f v[@p2] w[@p3]
intros; subst p2; subst p3; revert n v w p1.
A, B, C:Type
f:A -> B -> C
forall (n : nat) (v : t A n) (w : t B n)
  (p1 : Fin.t n), (map2 f v w)[@p1] = f v[@p1] w[@p1]
refine (@rect2 _ _ _ _ _); simpl.
A, B, C:Type
f:A -> B -> C
forall p1 : Fin.t 0,
match p1 in (Fin.t m') return (t C m' -> C) with
| @Fin.F1 n =>
    caseS (fun (n0 : nat) (_ : t C (S n0)) => C)
      (fun (h : C) (n0 : nat) (_ : t C n0) => h)
| @Fin.FS n p' =>
    fun v : t C (S n) =>
    caseS
      (fun (n0 : nat) (_ : t C (S n0)) =>
       Fin.t n0 -> C)
      (fun (_ : C) (n0 : nat) (t : t C n0)
         (p0 : Fin.t n0) => t[@p0]) v p'
end [] =
f
  (match p1 in (Fin.t m') return (t A m' -> A) with
   | @Fin.F1 n =>
       caseS (fun (n0 : nat) (_ : t A (S n0)) => A)
         (fun (h : A) (n0 : nat) (_ : t A n0) => h)
   | @Fin.FS n p' =>
       fun v : t A (S n) =>
       caseS
         (fun (n0 : nat) (_ : t A (S n0)) =>
          Fin.t n0 -> A)
         (fun (_ : A) (n0 : nat) (t : t A n0)
            (p0 : Fin.t n0) => t[@p0]) v p'
   end [])
  (match p1 in (Fin.t m') return (t B m' -> B) with
   | @Fin.F1 n =>
       caseS (fun (n0 : nat) (_ : t B (S n0)) => B)
         (fun (h : B) (n0 : nat) (_ : t B n0) => h)
   | @Fin.FS n p' =>
       fun v : t B (S n) =>
       caseS
         (fun (n0 : nat) (_ : t B (S n0)) =>
          Fin.t n0 -> B)
         (fun (_ : B) (n0 : nat) (t : t B n0)
            (p0 : Fin.t n0) => t[@p0]) v p'
   end [])
A, B, C:Type
f:A -> B -> C
forall (n : nat) (v1 : t A n) (v2 : t B n),
(forall p1 : Fin.t n,
 (map2 f v1 v2)[@p1] = f v1[@p1] v2[@p1]) ->
forall (a : A) (b : B) (p1 : Fin.t (S n)),
match p1 in (Fin.t m') return (t C m' -> C) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t C (S n1)) => C)
      (fun (h : C) (n1 : nat) (_ : t C n1) => h)
| @Fin.FS n0 p' =>
    fun v : t C (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t C (S n1)) =>
       Fin.t n1 -> C)
      (fun (_ : C) (n1 : nat) (t : t C n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (f a b :: map2 f v1 v2) =
f
  (match p1 in (Fin.t m') return (t A m' -> A) with
   | @Fin.F1 n0 =>
       caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
         (fun (h : A) (n1 : nat) (_ : t A n1) => h)
   | @Fin.FS n0 p' =>
       fun v : t A (S n0) =>
       caseS
         (fun (n1 : nat) (_ : t A (S n1)) =>
          Fin.t n1 -> A)
         (fun (_ : A) (n1 : nat) (t : t A n1)
            (p0 : Fin.t n1) => t[@p0]) v p'
   end (a :: v1))
  (match p1 in (Fin.t m') return (t B m' -> B) with
   | @Fin.F1 n0 =>
       caseS (fun (n1 : nat) (_ : t B (S n1)) => B)
         (fun (h : B) (n1 : nat) (_ : t B n1) => h)
   | @Fin.FS n0 p' =>
       fun v : t B (S n0) =>
       caseS
         (fun (n1 : nat) (_ : t B (S n1)) =>
          Fin.t n1 -> B)
         (fun (_ : B) (n1 : nat) (t : t B n1)
            (p0 : Fin.t n1) => t[@p0]) v p'
   end (b :: v2))
-
A, B, C:Type
f:A -> B -> C
forall p1 : Fin.t 0,
match p1 in (Fin.t m') return (t C m' -> C) with
| @Fin.F1 n =>
    caseS (fun (n0 : nat) (_ : t C (S n0)) => C)
      (fun (h : C) (n0 : nat) (_ : t C n0) => h)
| @Fin.FS n p' =>
    fun v : t C (S n) =>
    caseS
      (fun (n0 : nat) (_ : t C (S n0)) =>
       Fin.t n0 -> C)
      (fun (_ : C) (n0 : nat) (t : t C n0)
         (p0 : Fin.t n0) => t[@p0]) v p'
end [] =
f
  (match p1 in (Fin.t m') return (t A m' -> A) with
   | @Fin.F1 n =>
       caseS (fun (n0 : nat) (_ : t A (S n0)) => A)
         (fun (h : A) (n0 : nat) (_ : t A n0) => h)
   | @Fin.FS n p' =>
       fun v : t A (S n) =>
       caseS
         (fun (n0 : nat) (_ : t A (S n0)) =>
          Fin.t n0 -> A)
         (fun (_ : A) (n0 : nat) (t : t A n0)
            (p0 : Fin.t n0) => t[@p0]) v p'
   end [])
  (match p1 in (Fin.t m') return (t B m' -> B) with
   | @Fin.F1 n =>
       caseS (fun (n0 : nat) (_ : t B (S n0)) => B)
         (fun (h : B) (n0 : nat) (_ : t B n0) => h)
   | @Fin.FS n p' =>
       fun v : t B (S n) =>
       caseS
         (fun (n0 : nat) (_ : t B (S n0)) =>
          Fin.t n0 -> B)
         (fun (_ : B) (n0 : nat) (t : t B n0)
            (p0 : Fin.t n0) => t[@p0]) v p'
   end []) exact (Fin.case0 _).
-
A, B, C:Type
f:A -> B -> C
forall (n : nat) (v1 : t A n) (v2 : t B n),
(forall p1 : Fin.t n,
 (map2 f v1 v2)[@p1] = f v1[@p1] v2[@p1]) ->
forall (a : A) (b : B) (p1 : Fin.t (S n)),
match p1 in (Fin.t m') return (t C m' -> C) with
| @Fin.F1 n0 =>
    caseS (fun (n1 : nat) (_ : t C (S n1)) => C)
      (fun (h : C) (n1 : nat) (_ : t C n1) => h)
| @Fin.FS n0 p' =>
    fun v : t C (S n0) =>
    caseS
      (fun (n1 : nat) (_ : t C (S n1)) =>
       Fin.t n1 -> C)
      (fun (_ : C) (n1 : nat) (t : t C n1)
         (p0 : Fin.t n1) => t[@p0]) v p'
end (f a b :: map2 f v1 v2) =
f
  (match p1 in (Fin.t m') return (t A m' -> A) with
   | @Fin.F1 n0 =>
       caseS (fun (n1 : nat) (_ : t A (S n1)) => A)
         (fun (h : A) (n1 : nat) (_ : t A n1) => h)
   | @Fin.FS n0 p' =>
       fun v : t A (S n0) =>
       caseS
         (fun (n1 : nat) (_ : t A (S n1)) =>
          Fin.t n1 -> A)
         (fun (_ : A) (n1 : nat) (t : t A n1)
            (p0 : Fin.t n1) => t[@p0]) v p'
   end (a :: v1))
  (match p1 in (Fin.t m') return (t B m' -> B) with
   | @Fin.F1 n0 =>
       caseS (fun (n1 : nat) (_ : t B (S n1)) => B)
         (fun (h : B) (n1 : nat) (_ : t B n1) => h)
   | @Fin.FS n0 p' =>
       fun v : t B (S n0) =>
       caseS
         (fun (n1 : nat) (_ : t B (S n1)) =>
          Fin.t n1 -> B)
         (fun (_ : B) (n1 : nat) (t : t B n1)
            (p0 : Fin.t n1) => t[@p0]) v p'
   end (b :: v2)) intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
    now simpl.
Qed.

Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A}
  (assoc: forall a b c, f (f a b) c = f (f a c) b)
  {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a.
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a
Proof.
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a
assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
forall (n0 : nat) (h : B) (v0 : t B n0) (a : A),
fold_left f (f a h) v0 = f (fold_left f a v0) h
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
H:forall (n0 : nat) (h : B) (v0 : t B n0) (a : A),
fold_left f (f a h) v0 = f (fold_left f a v0) h
forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a
-
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
forall (n0 : nat) (h : B) (v0 : t B n0) (a : A),
fold_left f (f a h) v0 = f (fold_left f a v0) h induction v0.
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
h:B
forall a : A,
fold_left f (f a h) [] = f (fold_left f a []) h
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
h, h0:B
n0:nat
v0:t B n0
IHv0:forall a : A,
fold_left f (f a h) v0 = f (fold_left f a v0) h
forall a : A,
fold_left f (f a h) (h0 :: v0) =
f (fold_left f a (h0 :: v0)) h
  +
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
h:B
forall a : A,
fold_left f (f a h) [] = f (fold_left f a []) h now simpl.
  +
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
h, h0:B
n0:nat
v0:t B n0
IHv0:forall a : A,
fold_left f (f a h) v0 = f (fold_left f a v0) h
forall a : A,
fold_left f (f a h) (h0 :: v0) =
f (fold_left f a (h0 :: v0)) h intros; simpl.
A, B:Type
f:A -> B -> A
assoc:forall (a0 : A) (b c : B),
f (f a0 b) c = f (f a0 c) b
n:nat
v:t B n
h, h0:B
n0:nat
v0:t B n0
IHv0:forall a0 : A,
fold_left f (f a0 h) v0 =
f (fold_left f a0 v0) h
a:A
fold_left f (f (f a h) h0) v0 =
f (fold_left f (f a h0) v0) h rewrite<- IHv0, assoc.
A, B:Type
f:A -> B -> A
assoc:forall (a0 : A) (b c : B),
f (f a0 b) c = f (f a0 c) b
n:nat
v:t B n
h, h0:B
n0:nat
v0:t B n0
IHv0:forall a0 : A,
fold_left f (f a0 h) v0 =
f (fold_left f a0 v0) h
a:A
fold_left f (f (f a h0) h) v0 =
fold_left f (f (f a h0) h) v0 now f_equal.
-
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
n:nat
v:t B n
H:forall (n0 : nat) (h : B) (v0 : t B n0) (a : A),
fold_left f (f a h) v0 = f (fold_left f a v0) h
forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a induction v.
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
H:forall (n : nat) (h : B) (v : t B n) (a : A),
fold_left f (f a h) v = f (fold_left f a v) h
forall a : A,
fold_left f a [] =
fold_right (fun (x : B) (y : A) => f y x) [] a
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
h:B
n:nat
v:t B n
H:forall (n0 : nat) (h0 : B) (v0 : t B n0) (a : A),
fold_left f (f a h0) v0 = f (fold_left f a v0) h0
IHv:forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a
forall a : A,
fold_left f a (h :: v) =
fold_right (fun (x : B) (y : A) => f y x) (h :: v) a
  +
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
H:forall (n : nat) (h : B) (v : t B n) (a : A),
fold_left f (f a h) v = f (fold_left f a v) h
forall a : A,
fold_left f a [] =
fold_right (fun (x : B) (y : A) => f y x) [] a reflexivity.
  +
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
h:B
n:nat
v:t B n
H:forall (n0 : nat) (h0 : B) (v0 : t B n0) (a : A),
fold_left f (f a h0) v0 = f (fold_left f a v0) h0
IHv:forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a
forall a : A,
fold_left f a (h :: v) =
fold_right (fun (x : B) (y : A) => f y x) (h :: v) a simpl.
A, B:Type
f:A -> B -> A
assoc:forall (a : A) (b c : B),
f (f a b) c = f (f a c) b
h:B
n:nat
v:t B n
H:forall (n0 : nat) (h0 : B) (v0 : t B n0) (a : A),
fold_left f (f a h0) v0 = f (fold_left f a v0) h0
IHv:forall a : A,
fold_left f a v =
fold_right (fun (x : B) (y : A) => f y x) v a
forall a : A,
fold_left f (f a h) v =
f (fold_right (fun (x : B) (y : A) => f y x) v a) h intros; now rewrite<- (IHv).
Qed.

Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l.
A:Type
l:list A
to_list (of_list l) = l
Proof.
A:Type
l:list A
to_list (of_list l) = l
induction l.
A:Type
to_list (of_list Datatypes.nil) = Datatypes.nil
A:Type
a:A
l:list A
IHl:to_list (of_list l) = l
to_list (of_list (a :: l)) = (a :: l)%list
-
A:Type
to_list (of_list Datatypes.nil) = Datatypes.nil reflexivity.
-
A:Type
a:A
l:list A
IHl:to_list (of_list l) = l
to_list (of_list (a :: l)) = (a :: l)%list unfold to_list; simpl.
A:Type
a:A
l:list A
IHl:to_list (of_list l) = l
(a
 :: (fix
     fold_right_fix (n : nat) (v : t A n) (b : list A)
                    {struct v} : list A :=
       match v with
       | [] => b
       | cons _ a0 n0 w => a0 :: fold_right_fix n0 w b
       end) (length l) (of_list l) Datatypes.nil)%list =
(a :: l)%list now f_equal.
Qed.

Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = [].
forall (A : Type) (n : nat) (le : 0 <= n) (v : t A n),
take 0 le v = []
Proof.
forall (A : Type) (n : nat) (le : 0 <= n) (v : t A n),
take 0 le v = [] 
  reflexivity.
Qed. 

Lemma take_idem : forall {A} p n (v:t A n)  le le', 
  take p le' (take p le v) = take p le v.
forall (A : Type) (p n : nat) (v : t A n)
  (le : p <= n) (le' : p <= p),
take p le' (take p le v) = take p le v
Proof.
forall (A : Type) (p n : nat) (v : t A n)
  (le : p <= n) (le' : p <= p),
take p le' (take p le v) = take p le v 
  induction p; intros n v le le'.
A:Type
n:nat
v:t A n
le:0 <= n
le':0 <= 0
take 0 le' (take 0 le v) = take 0 le v
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 : p <= n0) (le'0 : p <= p),
take p le'0 (take p le0 v0) = take p le0 v0
n:nat
v:t A n
le:S p <= n
le':S p <= S p
take (S p) le' (take (S p) le v) = take (S p) le v
  -
A:Type
n:nat
v:t A n
le:0 <= n
le':0 <= 0
take 0 le' (take 0 le v) = take 0 le v auto. 
  -
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 : p <= n0) (le'0 : p <= p),
take p le'0 (take p le0 v0) = take p le0 v0
n:nat
v:t A n
le:S p <= n
le':S p <= S p
take (S p) le' (take (S p) le v) = take (S p) le v destruct v.
A:Type
p:nat
IHp:forall (n : nat) (v : t A n) (le0 : p <= n) (le'0 : p <= p),
take p le'0 (take p le0 v) = take p le0 v
le:S p <= 0
le':S p <= S p
take (S p) le' (take (S p) le []) = take (S p) le []
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 : p <= n0) (le'0 : p <= p),
take p le'0 (take p le0 v0) = take p le0 v0
h:A
n:nat
v:t A n
le:S p <= S n
le':S p <= S p
take (S p) le' (take (S p) le (h :: v)) =
take (S p) le (h :: v) inversion le.
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 : p <= n0) (le'0 : p <= p),
take p le'0 (take p le0 v0) = take p le0 v0
h:A
n:nat
v:t A n
le:S p <= S n
le':S p <= S p
take (S p) le' (take (S p) le (h :: v)) =
take (S p) le (h :: v) simpl.
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 : p <= n0) (le'0 : p <= p),
take p le'0 (take p le0 v0) = take p le0 v0
h:A
n:nat
v:t A n
le:S p <= S n
le':S p <= S p
h
:: take p (Le.le_S_n p p le')
     (take p (Le.le_S_n p n le) v) =
h :: take p (Le.le_S_n p n le) v apply f_equal.
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 : p <= n0) (le'0 : p <= p),
take p le'0 (take p le0 v0) = take p le0 v0
h:A
n:nat
v:t A n
le:S p <= S n
le':S p <= S p
take p (Le.le_S_n p p le')
  (take p (Le.le_S_n p n le) v) =
take p (Le.le_S_n p n le) v apply IHp. 
Qed.

Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v.
forall (A : Type) (n : nat) (v : t A n) (m : nat)
  (w : t A m) (le : n <= n + m),
take n le (v ++ w) = v
Proof.
forall (A : Type) (n : nat) (v : t A n) (m : nat)
  (w : t A m) (le : n <= n + m),
take n le (v ++ w) = v 
  induction v; intros m w le.
A:Type
m:nat
w:t A m
le:0 <= 0 + m
take 0 le ([] ++ w) = []
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (le0 : n <= n + m0), take n le0 (v ++ w0) = v
m:nat
w:t A m
le:S n <= S n + m
take (S n) le ((h :: v) ++ w) = h :: v
  -
A:Type
m:nat
w:t A m
le:0 <= 0 + m
take 0 le ([] ++ w) = [] reflexivity. 
  -
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (le0 : n <= n + m0), take n le0 (v ++ w0) = v
m:nat
w:t A m
le:S n <= S n + m
take (S n) le ((h :: v) ++ w) = h :: v simpl.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (le0 : n <= n + m0), take n le0 (v ++ w0) = v
m:nat
w:t A m
le:S n <= S n + m
h :: take n (Le.le_S_n n (n + m) le) (v ++ w) = h :: v apply f_equal.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (le0 : n <= n + m0), take n le0 (v ++ w0) = v
m:nat
w:t A m
le:S n <= S n + m
take n (Le.le_S_n n (n + m) le) (v ++ w) = v apply IHv. 
Qed.

(* Proof is irrelevant for [take] *)
Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v.
forall (A : Type) (p n : nat) (v : t A n)
  (le le' : p <= n), take p le v = take p le' v
Proof.
forall (A : Type) (p n : nat) (v : t A n)
  (le le' : p <= n), take p le v = take p le' v 
  induction p; intros n v le le'.
A:Type
n:nat
v:t A n
le, le':0 <= n
take 0 le v = take 0 le' v
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 le'0 : p <= n0),
take p le0 v0 = take p le'0 v0
n:nat
v:t A n
le, le':S p <= n
take (S p) le v = take (S p) le' v 
  -
A:Type
n:nat
v:t A n
le, le':0 <= n
take 0 le v = take 0 le' v reflexivity.  
  -
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 le'0 : p <= n0),
take p le0 v0 = take p le'0 v0
n:nat
v:t A n
le, le':S p <= n
take (S p) le v = take (S p) le' v destruct v.
A:Type
p:nat
IHp:forall (n : nat) (v : t A n) (le0 le'0 : p <= n),
take p le0 v = take p le'0 v
le, le':S p <= 0
take (S p) le [] = take (S p) le' []
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 le'0 : p <= n0),
take p le0 v0 = take p le'0 v0
h:A
n:nat
v:t A n
le, le':S p <= S n
take (S p) le (h :: v) = take (S p) le' (h :: v) inversion le.
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 le'0 : p <= n0),
take p le0 v0 = take p le'0 v0
h:A
n:nat
v:t A n
le, le':S p <= S n
take (S p) le (h :: v) = take (S p) le' (h :: v) simpl.
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 le'0 : p <= n0),
take p le0 v0 = take p le'0 v0
h:A
n:nat
v:t A n
le, le':S p <= S n
h :: take p (Le.le_S_n p n le) v =
h :: take p (Le.le_S_n p n le') v apply f_equal.
A:Type
p:nat
IHp:forall (n0 : nat) (v0 : t A n0) (le0 le'0 : p <= n0),
take p le0 v0 = take p le'0 v0
h:A
n:nat
v:t A n
le, le':S p <= S n
take p (Le.le_S_n p n le) v =
take p (Le.le_S_n p n le') v apply IHp. 
Qed.

Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n),
    uncons (a::v) = (a,v).
A:Type
forall (n : nat) (a : A) (v : t A n),
uncons (a :: v) = (a, v)
Proof.
A:Type
forall (n : nat) (a : A) (v : t A n),
uncons (a :: v) = (a, v) reflexivity. Qed.

Lemma append_comm_cons {A} : forall {n m : nat} (v : t A n) (w : t A m) (a : A),
    a :: (v ++ w) = (a :: v) ++ w.
A:Type
forall (n m : nat) (v : t A n) (w : t A m) (a : A),
a :: v ++ w = (a :: v) ++ w
Proof.
A:Type
forall (n m : nat) (v : t A n) (w : t A m) (a : A),
a :: v ++ w = (a :: v) ++ w reflexivity. Qed.

Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m),
    splitat n (v ++ w) = (v, w).
A:Type
forall (n m : nat) (v : t A n) (w : t A m),
splitat n (v ++ w) = (v, w)
Proof with simpl; auto.
A:Type
forall (n m : nat) (v : t A n) (w : t A m),
splitat n (v ++ w) = (v, w)
  intros n m v.
A:Type
n, m:nat
v:t A n
forall w : t A m, splitat n (v ++ w) = (v, w)
  generalize dependent m.
A:Type
n:nat
v:t A n
forall (m : nat) (w : t A m),
splitat n (v ++ w) = (v, w)
  induction v; intros...
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0), splitat n (v ++ w0) = (v, w0)
m:nat
w:t A m
(let (v1, v2) := splitat n (v ++ w) in (h :: v1, v2)) =
(h :: v, w)
  rewrite IHv...
Qed.

Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A (n+m)),
    splitat n vw = (v, w) ->
    vw = v ++ w.
A:Type
forall (n m : nat) (v : t A n) (w : t A m)
  (vw : t A (n + m)),
splitat n vw = (v, w) -> vw = v ++ w
Proof with auto.
A:Type
forall (n m : nat) (v : t A n) (w : t A m)
  (vw : t A (n + m)),
splitat n vw = (v, w) -> vw = v ++ w
  intros n m v.
A:Type
n, m:nat
v:t A n
forall (w : t A m) (vw : t A (n + m)),
splitat n vw = (v, w) -> vw = v ++ w
  generalize dependent m.
A:Type
n:nat
v:t A n
forall (m : nat) (w : t A m) (vw : t A (n + m)),
splitat n vw = (v, w) -> vw = v ++ w
  induction v; intros; inversion H...
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
H1:(let (v1, v2) := splitat n (tl vw) in
 (hd vw :: v1, v2)) = (h :: v, w)
vw = (h :: v) ++ w
  destruct (splitat n (tl vw)) as [v' w'] eqn:Heq.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
v':t A n
w':t A m
Heq:splitat n (tl vw) = (v', w')
H1:(hd vw :: v', w') = (h :: v, w)
vw = (h :: v) ++ w
  apply pair_equal_spec in H1.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
v':t A n
w':t A m
Heq:splitat n (tl vw) = (v', w')
H1:hd vw :: v' = h :: v /\ w' = w
vw = (h :: v) ++ w
  destruct H1; subst.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
v':t A n
Heq:splitat n (tl vw) = (v', w)
H0:hd vw :: v' = h :: v
vw = (h :: v) ++ w
  rewrite <- append_comm_cons.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
v':t A n
Heq:splitat n (tl vw) = (v', w)
H0:hd vw :: v' = h :: v
vw = h :: v ++ w
  rewrite (eta vw).
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
v':t A n
Heq:splitat n (tl vw) = (v', w)
H0:hd vw :: v' = h :: v
hd vw :: tl vw = h :: v ++ w
  apply cons_inj in H0.
A:Type
h:A
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (h :: v, w)
v':t A n
Heq:splitat n (tl vw) = (v', w)
H0:hd vw = h /\ v' = v
hd vw :: tl vw = h :: v ++ w
  destruct H0; subst.
A:Type
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (hd vw :: v, w)
Heq:splitat n (tl vw) = (v, w)
hd vw :: tl vw = hd vw :: v ++ w
  f_equal...
A:Type
n:nat
v:t A n
IHv:forall (m0 : nat) (w0 : t A m0) (vw0 : t A (n + m0)),
splitat n vw0 = (v, w0) -> vw0 = v ++ w0
m:nat
w:t A m
vw:t A (S n + m)
H:splitat (S n) vw = (hd vw :: v, w)
Heq:splitat n (tl vw) = (v, w)
tl vw = v ++ w
  apply IHv...
Qed.