val parser_kind_prop_ext
  (#t: Type)
  (k: parser_kind)
  (f1 f2: bare_parser t)
: Lemma
  (requires (forall (input: bytes) . parse f1 input == parse f2 input))
  (ensures (parser_kind_prop k f1 <==> parser_kind_prop k f2))
let parser_kind_prop_ext
  (#t: Type)
  (k: parser_kind)
  (f1 f2: bare_parser t)
: Lemma
  (requires (forall (input: bytes) . parse f1 input == parse f2 input))
  (ensures (parser_kind_prop k f1 <==> parser_kind_prop k f2))
= no_lookahead_ext f1 f2;
  injective_ext f1 f2
val parser_kind_prop_ext
  (#t: Type)
  (k: parser_kind)
  (f1 f2: bare_parser t)
: Lemma
  (requires (forall (input: bytes) . parse f1 input == parse f2 input))
  (ensures (parser_kind_prop k f1 <==> parser_kind_prop k f2))
let parser_kind_prop_ext (#t: Type) (k: parser_kind) (f1 f2: bare_parser t)
    : Lemma (requires (forall (input: bytes). parse f1 input == parse f2 input))
      (ensures (parser_kind_prop k f1 <==> parser_kind_prop k f2)) =
no_lookahead_ext f1 f2;
injective_ext f1 f2
LowParse.Spec.Base.fst.checked
prims.fst.checked LowParse.Bytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Base.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.bare_parser LowParse.Spec.Base.injective_ext Prims.unit LowParse.Spec.Base.no_lookahead_ext Prims.l_Forall LowParse.Bytes.bytes Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse Prims.squash Prims.l_iff LowParse.Spec.Base.parser_kind_prop Prims.Nil FStar.Pervasives.pattern
module LowParse.Spec.Base
include LowParse.Bytes

module Seq = FStar.Seq
module U8 = FStar.UInt8
module U32 = FStar.UInt32

let parser_kind_prop = parser_kind_prop'

let parser_kind_prop_equiv
  (#t: Type) (k: parser_kind) (f: bare_parser t)
: Lemma
  (parser_kind_prop k f <==> parser_kind_prop' k f)
= ()

let parser_kind_prop_ext
  (#t: Type)
  (k: parser_kind)
  (f1 f2: bare_parser t)
: Lemma
  (requires (forall (input: bytes) . parse f1 input == parse f2 input))
val parser_kind_prop_ext
  (#t: Type)
  (k: parser_kind)
  (f1 f2: bare_parser t)
: Lemma
  (requires (forall (input: bytes) . parse f1 input == parse f2 input))
  (ensures (parser_kind_prop k f1 <==> parser_kind_prop k f2))

    k: LowParse.Spec.Base.parser_kind ->
    f1: LowParse.Spec.Base.bare_parser t ->
    f2: LowParse.Spec.Base.bare_parser t
  -> FStar.Pervasives.Lemma
      (requires
        forall (input: LowParse.Bytes.bytes).
          LowParse.Spec.Base.parse f1 input == LowParse.Spec.Base.parse f2 input)
      (ensures
        LowParse.Spec.Base.parser_kind_prop k f1 <==> LowParse.Spec.Base.parser_kind_prop k f2)