val synth_asn1_ASN1_NULL_TLV_inverse_impl (x: datatype_of_asn1_type ASN1_NULL)
    : Tot
    (a:
      ((the_asn1_tag ASN1_NULL & asn1_value_int32_of_type ASN1_NULL) &
        datatype_of_asn1_type ASN1_NULL){a == synth_asn1_ASN1_NULL_TLV_inverse x})
val synth_asn1_ASN1_NULL_TLV_inverse_impl (x: datatype_of_asn1_type ASN1_NULL)
    : Tot
    (a:
      ((the_asn1_tag ASN1_NULL & asn1_value_int32_of_type ASN1_NULL) &
        datatype_of_asn1_type ASN1_NULL){a == synth_asn1_ASN1_NULL_TLV_inverse x})
let synth_asn1_ASN1_NULL_TLV_inverse_impl
  (x: datatype_of_asn1_type ASN1_NULL)
: Tot (a: ((the_asn1_tag ASN1_NULL & asn1_value_int32_of_type ASN1_NULL) & datatype_of_asn1_type ASN1_NULL){a == synth_asn1_ASN1_NULL_TLV_inverse x})
= ((ASN1_NULL, 0ul), x)
module ASN1.Low.Value.NULL

open ASN1.Base
open ASN1.Spec.Value.NULL
open ASN1.Low.Base

open FStar.Integers

module B = LowStar.Buffer

friend ASN1.Spec.Value.NULL

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length` *)

let serialize32_asn1_ASN1_NULL_backwards ()
= fun (_: datatype_of_asn1_type ASN1_NULL)
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
-> 0ul

open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Low.Tag
open ASN1.Low.Length
/
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Value.NULL.fst.checked ASN1.Spec.Value.NULL.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.NULL.fst
x: ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL
  -> a:
    ((ASN1.Base.the_asn1_tag ASN1.Base.ASN1_NULL *
      ASN1.Base.asn1_value_int32_of_type ASN1.Base.ASN1_NULL) *
      ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL)
      {a == ASN1.Spec.Value.NULL.synth_asn1_ASN1_NULL_TLV_inverse x}
ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.asn1_value_int32_of_type FStar.UInt32.__uint_to_t Prims.eq2 ASN1.Spec.Value.NULL.synth_asn1_ASN1_NULL_TLV_inverse
let synth_asn1_ASN1_NULL_TLV_inverse_impl (x: datatype_of_asn1_type ASN1_NULL)
    : Tot
    (a:
      ((the_asn1_tag ASN1_NULL & asn1_value_int32_of_type ASN1_NULL) &
        datatype_of_asn1_type ASN1_NULL){a == synth_asn1_ASN1_NULL_TLV_inverse x}) =
  
((ASN1_NULL, 0ul), x)