val list_append_index (#a:Type) (x y:list a) (i:nat) : Lemma
  (requires i < List.length (x @ y))
  (ensures (
    let nx = List.length x in
    (i >= nx ==> i - nx < List.length y) /\
    List.index (x @ y) i == (if i < nx then List.index x i else List.index y (i - nx))
  ))
let rec list_append_index #a x y i =
  match x with
  | [] -> ()
  | h::t -> (if i > 0 then list_append_index t y (i - 1))
val list_append_index (#a:Type) (x y:list a) (i:nat) : Lemma
  (requires i < List.length (x @ y))
  (ensures (
    let nx = List.length x in
    (i >= nx ==> i - nx < List.length y) /\
    List.index (x @ y) i == (if i < nx then List.index x i else List.index y (i - nx))
  ))
let rec list_append_index #a x y i =
match x with
| [] -> ()
| h :: t -> (if i > 0 then list_append_index t y (i - 1))
Vale.Lib.Lists.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.Classical.fsti.checked
Vale.Lib.Lists.fst
Prims.list Prims.nat Prims.op_GreaterThan Vale.Lib.Lists.list_append_index Prims.op_Subtraction Prims.bool Prims.unit
module Vale.Lib.Lists
open FStar.Mul

#reset-options "--initial_fuel 2 --max_fuel 2"
let singleton_list_rev #a x = ()
let list_cons_is_append #a h t = ()

let singleton_list_seq #a x =
  lemma_seq_of_list_index [x] 0;
  assert (equal (seq_of_list [x]) (create 1 x))
#reset-options

let rec list_append_length #a x y =
  match x with
  | [] -> ()
  | _::t -> list_append_length t y
val list_append_index (#a:Type) (x y:list a) (i:nat) : Lemma
  (requires i < List.length (x @ y))
  (ensures (
    let nx = List.length x in
    (i >= nx ==> i - nx < List.length y) /\
    List.index (x @ y) i == (if i < nx then List.index x i else List.index y (i - nx))
  ))
x: Prims.list a -> y: Prims.list a -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires i < FStar.List.Tot.Base.length (x @ y))
      (ensures
        (let nx = FStar.List.Tot.Base.length x in
          (i >= nx ==> i - nx < FStar.List.Tot.Base.length y) /\
          FStar.List.Tot.Base.index (x @ y) i ==
          ((match i < nx with
              | true -> FStar.List.Tot.Base.index x i
              | _ -> FStar.List.Tot.Base.index y (i - nx))
            <:
            a)))