val lemma_synth_keyShareEntry_is_injective: Prims.unit
  -> Lemma (LP.synth_injective synth_keyShareEntry)
val lemma_synth_keyShareEntry_is_injective: Prims.unit
  -> Lemma (LP.synth_injective synth_keyShareEntry)
let lemma_synth_keyShareEntry_is_injective () 
  : Lemma (LP.synth_injective synth_keyShareEntry) 
  = LP.synth_injective_intro synth_keyShareEntry
module MiTLS.Format.KeyShareEntry
open MiTLS

open MiTLS.Parsers.NamedGroup
open MiTLS.Format.UncompressedPointRepresentation

module B = FStar.Bytes
module LP = LowParse.SLow
module U32 = FStar.UInt32


(* Parsers, validators *)

inline_for_extraction
let synth_keyShareEntry (r:namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)): Tot keyShareEntry = { group=(fst r); key_exchange=(snd r) }

inline_for_extraction
let unsynth_keyShareEntry (e:keyShareEntry): Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)) = e.group, e.key_exchange
/
prims.fst.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Format.UncompressedPointRepresentation.fsti.checked LowParse.Spec.Bytes.fst.checked LowParse.SLow.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Format.KeyShareEntry.fst
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Combinators.synth_injective MiTLS.Format.KeyShareEntry.synth_keyShareEntry)
Prims.unit LowParse.Spec.Combinators.synth_injective_intro FStar.Pervasives.Native.tuple2 MiTLS.Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t MiTLS.Format.KeyShareEntry.keyShareEntry MiTLS.Format.KeyShareEntry.synth_keyShareEntry Prims.l_True Prims.squash LowParse.Spec.Combinators.synth_injective Prims.Nil FStar.Pervasives.pattern
let lemma_synth_keyShareEntry_is_injective () : Lemma (LP.synth_injective synth_keyShareEntry) =
  
LP.synth_injective_intro synth_keyShareEntry