Lvc.Infra.Sublist

Require Import Plus List Get.

Inductive subList {X : Type} (L : list X) : list X → nat → Prop :=
| SubListNil n : subList L nil n
| SubListCons l L´ n : get L n l → subList L L´ (S n) → subList L (l::L´) n.

Lemma subList_app_r {X:Type} (P:list X) P1 P2 n:
subList P (P1++P2) n → subList P P2 (n+length P1).

Lemma subList_app_l {X:Type} (P:list X) P1 P2 n:
subList P (P1++P2) n → subList P P1 n.

Lemma subList_refl´ {X:Type} (L1 L2: list X):
subList (L1++L2) L2 (length L1).

Lemma subList_refl {X:Type} (L: list X) :
subList L L 0.