val seq_list_match_cons0
      (#t #t': Type)
      (c: Seq.seq t)
      (l: list t' {Cons? l})
      (item_match: (t -> v': t'{v' << l} -> vprop))
      (seq_list_match:
          (
                Seq.seq t ->
                v': list t' ->
                raw_data_item_match: (t -> v'': t'{v'' << v'} -> vprop){v' << l}
              -> vprop))
    : Tot vprop
let seq_list_match_cons0
  (#t #t': Type)
  (c: Seq.seq t)
  (l: list t' { Cons? l })
  (item_match: (t -> (v': t' { v' << l }) -> vprop))
  (seq_list_match: (Seq.seq t -> (v': list t') -> (raw_data_item_match: (t -> (v'': t' { v'' << v' }) -> vprop) { v' << l }) ->
vprop))
: Tot vprop
= exists_ (fun (c1: t) -> exists_ (fun (c2: Seq.seq t) ->
    item_match c1 (List.Tot.hd l) `star`
    seq_list_match c2 (List.Tot.tl l) item_match `star`
    pure (c `Seq.equal` Seq.cons c1 c2)
  ))
val seq_list_match_cons0
      (#t #t': Type)
      (c: Seq.seq t)
      (l: list t' {Cons? l})
      (item_match: (t -> v': t'{v' << l} -> vprop))
      (seq_list_match:
          (
                Seq.seq t ->
                v': list t' ->
                raw_data_item_match: (t -> v'': t'{v'' << v'} -> vprop){v' << l}
              -> vprop))
    : Tot vprop
let seq_list_match_cons0
      (#t #t': Type)
      (c: Seq.seq t)
      (l: list t' {Cons? l})
      (item_match: (t -> v': t'{v' << l} -> vprop))
      (seq_list_match:
          (
                Seq.seq t ->
                v': list t' ->
                raw_data_item_match: (t -> v'': t'{v'' << v'} -> vprop){v' << l}
              -> vprop))
    : Tot vprop =
exists_ (fun (c1: t) ->
      exists_ (fun (c2: Seq.seq t) ->
            ((item_match c1 (List.Tot.hd l)) `star` (seq_list_match c2 (List.Tot.tl l) item_match))
            `star`
            (pure (c `Seq.equal` (Seq.cons c1 c2)))))
Steel.ST.SeqMatch.fst.checked
Steel.ST.OnRange.fsti.checked Steel.ST.GenElim.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Steel.ST.SeqMatch.fst
FStar.Seq.Base.seq Prims.list Prims.b2t Prims.uu___is_Cons Prims.precedes Steel.Effect.Common.vprop Steel.ST.Util.exists_ Steel.Effect.Common.star FStar.List.Tot.Base.hd FStar.List.Tot.Base.tl Steel.ST.Util.pure FStar.Seq.Base.equal FStar.Seq.Properties.cons
module Steel.ST.SeqMatch
include Steel.ST.OnRange
open Steel.ST.GenElim

module Seq = FStar.Seq
module SZ = FStar.SizeT

(* `seq_list_match` describes how to match a sequence of low-level
values (the low-level contents of an array) with a list of high-level
values. `seq_list_match` is carefully designed to be usable within
(mutually) recursive definitions of matching functions on the type of
high-level values.  *)

[@@__reduce__]
let seq_list_match_nil0
  (#t: Type)
  (c: Seq.seq t)
: Tot vprop
= pure (c `Seq.equal` Seq.empty)

[@@__reduce__]
let seq_list_match_cons0
  (#t #t': Type)
  (c: Seq.seq t)
  (l: list t' { Cons? l })
  (item_match: (t -> (v': t' { v' << l }) -> vprop))
  (seq_list_match: (Seq.seq t -> (v': list t') -> (raw_data_item_match: (t -> (v'': t' { v'' << v' }) -> vprop) { v' << l }) ->
vprop))
val seq_list_match_cons0
      (#t #t': Type)
      (c: Seq.seq t)
      (l: list t' {Cons? l})
      (item_match: (t -> v': t'{v' << l} -> vprop))
      (seq_list_match:
          (
                Seq.seq t ->
                v': list t' ->
                raw_data_item_match: (t -> v'': t'{v'' << v'} -> vprop){v' << l}
              -> vprop))
    : Tot vprop

    c: FStar.Seq.Base.seq t ->
    l: Prims.list t' {Cons? l} ->
    item_match: (_: t -> v': t'{v' << l} -> Steel.Effect.Common.vprop) ->
    seq_list_match:
      (
            _: FStar.Seq.Base.seq t ->
            v': Prims.list t' ->
            raw_data_item_match: (_: t -> v'': t'{v'' << v'} -> Steel.Effect.Common.vprop){v' << l}
          -> Steel.Effect.Common.vprop)
  -> Steel.Effect.Common.vprop