let live4 #a #len (h:mem) (b0 b1 b2 b3: lbuffer a len) =
  live h b0 /\ live h b1 /\ live h b2 /\ live h b3
let live4
      #a
      #len
      (h: mem)
      (b0: lbuffer a len)
      (b1: lbuffer a len)
      (b2: lbuffer a len)
      (b3: lbuffer a len)
     =
live h b0 /\ live h b1 /\ live h b2 /\ live h b3
Lib.MultiBuffer.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.NTuple.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Lib.MultiBuffer.fst
Lib.IntTypes.size_t FStar.Monotonic.HyperStack.mem Lib.Buffer.lbuffer Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Prims.logical
module Lib.MultiBuffer

open FStar.Mul
module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All

open Lib.IntTypes
open Lib.Sequence
open Lib.Buffer
open Lib.NTuple

#set-options "--z3rlimit 30 --fuel 0 --ifuel 0"
val live4 : h: FStar.Monotonic.HyperStack.mem ->
    b0: Lib.Buffer.lbuffer a len ->
    b1: Lib.Buffer.lbuffer a len ->
    b2: Lib.Buffer.lbuffer a len ->
    b3: Lib.Buffer.lbuffer a len
  -> Prims.logical

    h: FStar.Monotonic.HyperStack.mem ->
    b0: Lib.Buffer.lbuffer a len ->
    b1: Lib.Buffer.lbuffer a len ->
    b2: Lib.Buffer.lbuffer a len ->
    b3: Lib.Buffer.lbuffer a len
  -> Prims.logical