val append_list_seq (#a:Type) (x y:list a) : Lemma
  (seq_of_list (x @ y) == append (seq_of_list x) (seq_of_list y))
let append_list_seq #a x y =
  list_append_length x y;
  let n = List.length (x @ y) in
  let index_of_x_y (i:nat{i < n}) : a = index (seq_of_list (x @ y)) i in
  let index_of_append_x_y (i:nat{i < n}) : a = index (append (seq_of_list x) (seq_of_list y)) i in
  let f (i:nat{i < n}) : Lemma (index_of_x_y i == index_of_append_x_y i) =
    list_append_index x y i;
    lemma_seq_of_list_index (x @ y) i;
    (
      if i < List.length x then
        lemma_seq_of_list_index x i
      else
        lemma_seq_of_list_index y (i - List.length x)
    )
    in
  FStar.Classical.forall_intro f;
  assert (equal (seq_of_list (x @ y)) (append (seq_of_list x) (seq_of_list y)))
val append_list_seq (#a:Type) (x y:list a) : Lemma
  (seq_of_list (x @ y) == append (seq_of_list x) (seq_of_list y))
let append_list_seq #a x y =
list_append_length x y;
let n = List.length (x @ y) in
let index_of_x_y (i: nat{i < n}) : a = index (seq_of_list (x @ y)) i in
let index_of_append_x_y (i: nat{i < n}) : a = index (append (seq_of_list x) (seq_of_list y)) i in
let f (i: nat{i < n}) : Lemma (index_of_x_y i == index_of_append_x_y i) =
  list_append_index x y i;
  lemma_seq_of_list_index (x @ y) i;
  (if i < List.length x
    then lemma_seq_of_list_index x i
    else lemma_seq_of_list_index y (i - List.length x))
in
FStar.Classical.forall_intro f;
assert (equal (seq_of_list (x @ y)) (append (seq_of_list x) (seq_of_list 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 Prims._assert FStar.Seq.Base.equal FStar.Seq.Properties.seq_of_list FStar.List.Tot.Base.op_At FStar.Seq.Base.append Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan Prims.eq2 Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern FStar.List.Tot.Base.length FStar.Seq.Properties.lemma_seq_of_list_index Prims.bool Prims.op_Subtraction Vale.Lib.Lists.list_append_index FStar.Seq.Base.index Vale.Lib.Lists.list_append_length
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

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 append_list_seq (#a:Type) (x y:list a) : Lemma
  (seq_of_list (x @ y) == append (seq_of_list x) (seq_of_list y))
x: Prims.list a -> y: Prims.list a
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Properties.seq_of_list (x @ y) ==
      FStar.Seq.Base.append (FStar.Seq.Properties.seq_of_list x)
        (FStar.Seq.Properties.seq_of_list y))