val lemma_synth_big_integer_as_octet_string_injective
  (len: asn1_value_int32_of_big_integer)
: Lemma (
  synth_injective (synth_big_integer_as_octet_string len)
)
val lemma_synth_big_integer_as_octet_string_injective
  (len: asn1_value_int32_of_big_integer)
: Lemma (
  synth_injective (synth_big_integer_as_octet_string len)
)
let lemma_synth_big_integer_as_octet_string_injective len
= synth_injective_intro'
  (* f *) (synth_big_integer_as_octet_string len)
  (*prf*) (lemma_synth_big_integer_as_octet_string_injective' len)
module ASN1.Spec.Value.BigInteger

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Bytes32

open FStar.Integers

module B32 = FStar.Bytes

let lemma_synth_big_integer_as_octet_string_injective'
  (len: asn1_value_int32_of_big_integer)
  (s32 s32': parse_filter_refine (filter_big_integer_as_octet_string len))
: Lemma
  (requires synth_big_integer_as_octet_string len s32 == synth_big_integer_as_octet_string len s32')
  (ensures s32 == s32')
= if (v len = 1) then
  ( () )
  else if (s32 `B32.index` 0 = 0x00uy) then
  ( assert (B32.length s32 == B32.length s32');
    assert (s32' `B32.index` 0 == 0x00uy);
    assert (s32 `B32.index` 0 == s32' `B32.index` 0);
    assert (B32.slice s32 1ul len `B32.equal` B32.slice s32' 1ul len);
    assert (forall (i: UInt32.t { 1 <= v i /\ v i < v (B32.length s32 )}). s32  `B32.get` i == B32.slice s32  1ul len `B32.get` (i - 1ul) );
    assert (forall (i: UInt32.t { 1 <= v i /\ v i < v (B32.length s32')}). s32' `B32.get` i == B32.slice s32' 1ul len `B32.get` (i - 1ul) );
    assert (s32 `B32.equal` s32');
    B32.extensionality s32 s32' )
  else
  ( () )
/
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Bytes32.fst.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.BigInteger.fst
len: ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Combinators.synth_injective (ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string
            len))
ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer LowParse.Spec.Combinators.synth_injective_intro' LowParse.Spec.Combinators.parse_filter_refine FStar.Bytes.lbytes32 ASN1.Spec.Value.BigInteger.filter_big_integer_as_octet_string ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t ASN1.Spec.Value.BigInteger.valid_big_integer_as_octet_string_prop ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string ASN1.Spec.Value.BigInteger.lemma_synth_big_integer_as_octet_string_injective' Prims.unit
let lemma_synth_big_integer_as_octet_string_injective len =
  
synth_injective_intro' (synth_big_integer_as_octet_string len)
  (lemma_synth_big_integer_as_octet_string_injective' len)