val sel4 (#a: Type) (m: map4 a) (n: int) : a
let sel4 (#a:Type) (m:map4 a) (n:int) : a =
  match m with (m0, m1) ->
  match n < 2 with true -> sel2 m0 n | false -> sel2 m1 (n - 2)
val sel4 (#a: Type) (m: map4 a) (n: int) : a
let sel4 (#a: Type) (m: map4 a) (n: int) : a =
match m with
| m0, m1 ->
  match n < 2 with
  | true -> sel2 m0 n
  | false -> sel2 m1 (n - 2)
Vale.Lib.Map16.fsti.checked
Vale.X64.Machine_s.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Lib.Map16.fsti
Vale.Lib.Map16.map4 Prims.int Vale.Lib.Map16.map2 Prims.op_LessThan Vale.Lib.Map16.sel2 Prims.op_Subtraction
module Vale.Lib.Map16
open FStar.Mul
open Vale.X64.Machine_s

type map2 (a:Type) = a & a
type map4 (a:Type) = map2 a & map2 a
type map8 (a:Type) = map4 a & map4 a
type map16 (a:Type) = map8 a & map8 a

[@va_qattr]
let sel2 (#a:Type) (m:map2 a) (n:int) : a =
  match m with (m0, m1) ->
  match n < 1 with true -> m0 | false -> m1

[@va_qattr]
val sel4 (#a: Type) (m: map4 a) (n: int) : a
m: Vale.Lib.Map16.map4 a -> n: Prims.int -> a