val map_dec (top: 'a) (l: list 'b {l << top}) (f: (x: 'b{x << l} -> 'c)) : list 'c
let rec map_dec (top:'a) (l : list 'b{l << top}) (f : (x:'b{x << l} -> 'c)) : list 'c =
  match l with
  | [] -> []
  | x::xs -> f x :: map_dec top xs f
val map_dec (top: 'a) (l: list 'b {l << top}) (f: (x: 'b{x << l} -> 'c)) : list 'c
let rec map_dec (top: 'a) (l: list 'b {l << top}) (f: (x: 'b{x << l} -> 'c)) : list 'c =
match l with
| [] -> []
| x :: xs -> f x :: map_dec top xs f
Pulse.Common.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Pulse.Common.fst
Prims.list Prims.precedes Prims.Nil Prims.Cons Pulse.Common.map_dec
module Pulse.Common

module L = FStar.List.Tot
open FStar.Tactics

let (let?) (f:option 'a) (g:'a -> option 'b) : option 'b =
  match f with
  | None -> None
  | Some x -> g x

// let lem_bind_opt_some (x : option 'a) (f : 'a -> option 'b)
//   : Lemma (requires Some? ((let?) x f))
//           (ensures Some? x /\ Some? (f (Some?.v x)))
//           [SMTPat (Some? ((let?) x f))]
//   = ()

// let lem_bind_opt_none (x : option 'a) (f : 'a -> option 'b)
//   : Lemma (requires None? ((let?) x f))
//           (ensures None? x \/ None? (f (Some?.v x)))
//           [SMTPat (Some? ((let?) x f))]
//   = ()

let rec for_all_dec (top:'a) (l : list 'b{l << top}) (f : (x:'b{x << l} -> bool)) : bool =
  match l with
  | [] -> true
  | x::xs -> f x && for_all_dec top xs f
val map_dec (top: 'a) (l: list 'b {l << top}) (f: (x: 'b{x << l} -> 'c)) : list 'c
top: 'a -> l: Prims.list 'b {l << top} -> f: (x: 'b{x << l} -> 'c) -> Prims.list 'c