val from_list_be (l: list bool) : int
let from_list_be (l:list bool) : int =
  from_list_le (List.rev l)
val from_list_be (l: list bool) : int
let from_list_be (l: list bool) : int =
from_list_le (List.rev l)
Vale.Lib.Lists.fsti.checked
prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.fst.checked
Vale.Lib.Lists.fsti
Prims.list Prims.bool Vale.Lib.Lists.from_list_le FStar.List.Tot.Base.rev Prims.int
module Vale.Lib.Lists

open FStar.List.Tot
open FStar.Seq
open FStar.UInt
open FStar.Mul
module List = FStar.List.Tot
open FStar.List.Tot.Properties

val singleton_list_rev (#a:Type) (x:a) : Lemma
  (List.rev [x] == [x])

val list_cons_is_append (#a:Type) (h:a) (t:list a) : Lemma
  (h::t == [h] @ t)

val singleton_list_seq (#a:Type) (x:a) : Lemma
  (seq_of_list [x] == create 1 x)

val list_append_length (#a:Type) (x y:list a) : Lemma
  (List.length (x @ y) == List.length x + List.length 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))
  ))

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 rec from_list_le (l:list bool) : int =
  match l with
  | [] -> 0
  | h::t -> (if h then 1 else 0) + 2 * (from_list_le t)
val from_list_be (l: list bool) : int
l: Prims.list Prims.bool -> Prims.int