val singleton_list_seq (#a:Type) (x:a) : Lemma
  (seq_of_list [x] == create 1 x)
let singleton_list_seq #a x =
  lemma_seq_of_list_index [x] 0;
  assert (equal (seq_of_list [x]) (create 1 x))
val singleton_list_seq (#a:Type) (x:a) : Lemma
  (seq_of_list [x] == create 1 x)
let singleton_list_seq #a x =
lemma_seq_of_list_index [x] 0;
assert (equal (seq_of_list [x]) (create 1 x))
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._assert FStar.Seq.Base.equal FStar.Seq.Properties.seq_of_list Prims.Cons Prims.Nil FStar.Seq.Base.create Prims.unit FStar.Seq.Properties.lemma_seq_of_list_index
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 = ()
val singleton_list_seq (#a:Type) (x:a) : Lemma
  (seq_of_list [x] == create 1 x)
x: a
  -> FStar.Pervasives.Lemma
    (ensures FStar.Seq.Properties.seq_of_list [x] == FStar.Seq.Base.create 1 x)