val 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')
val 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')
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
  ( () )
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
/
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 ->
    s32:
      LowParse.Spec.Combinators.parse_filter_refine (ASN1.Spec.Value.BigInteger.filter_big_integer_as_octet_string
            len) ->
    s32':
      LowParse.Spec.Combinators.parse_filter_refine (ASN1.Spec.Value.BigInteger.filter_big_integer_as_octet_string
            len)
  -> FStar.Pervasives.Lemma
      (requires
        ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string len s32 ==
        ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string len s32') (ensures s32 == s32')
ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer LowParse.Spec.Combinators.parse_filter_refine FStar.Bytes.lbytes32 ASN1.Spec.Value.BigInteger.filter_big_integer_as_octet_string Prims.op_Equality Prims.int FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 Prims.bool FStar.UInt8.t FStar.Bytes.index FStar.UInt8.__uint_to_t FStar.Bytes.extensionality Prims.unit Prims._assert FStar.Bytes.equal Prims.l_Forall FStar.UInt32.t Prims.l_and Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.op_Less FStar.Bytes.length Prims.eq2 FStar.Bytes.byte FStar.Bytes.get FStar.Bytes.slice FStar.UInt32.__uint_to_t FStar.Integers.op_Subtraction FStar.UInt.uint_t ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t Prims.l_or ASN1.Spec.Value.BigInteger.valid_big_integer_as_octet_string_prop ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string Prims.squash Prims.Nil FStar.Pervasives.pattern
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 (())