val list_append_length (#a:Type) (x y:list a) : Lemma
  (List.length (x @ y) == List.length x + List.length y)
let rec list_append_length #a x y =
  match x with
  | [] -> ()
  | _::t -> list_append_length t y
val list_append_length (#a:Type) (x y:list a) : Lemma
  (List.length (x @ y) == List.length x + List.length y)
let rec list_append_length #a x y =
match x with
| [] -> ()
| _ :: t -> list_append_length t y
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 Vale.Lib.Lists.list_append_length 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
val list_append_length (#a:Type) (x y:list a) : Lemma
  (List.length (x @ y) == List.length x + List.length y)
x: Prims.list a -> y: Prims.list a
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.List.Tot.Base.length (x @ y) ==
      FStar.List.Tot.Base.length x + FStar.List.Tot.Base.length y)