val coerce_parser_serializer
      (#t2: Type0)
      (#k: parser_kind)
      (#t1: Type0)
      (#p1: parser k t1)
      (p2: parser k t2)
      (s: serializer p1)
      (u: unit{t2 == t1 /\ p2 == coerce_parser t2 p1})
    : Tot (serializer (p2))
val coerce_parser_serializer
      (#t2: Type0)
      (#k: parser_kind)
      (#t1: Type0)
      (#p1: parser k t1)
      (p2: parser k t2)
      (s: serializer p1)
      (u: unit{t2 == t1 /\ p2 == coerce_parser t2 p1})
    : Tot (serializer (p2))
let coerce_parser_serializer
  (#t2: Type0)
  (#k: parser_kind)
  (#t1: Type0)
  (#p1: parser k t1)
  (p2: parser k t2)
  (s: serializer p1)
  (u: unit { t2 == t1 /\ p2 == coerce_parser t2 p1} )
: Tot (serializer (p2))
= s
module ASN1.Spec.Base

include LowParse.Spec.Base
include LowParse.Spec.Combinators
/
prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
ASN1.Spec.Base.fst

    p2: LowParse.Spec.Base.parser k t2 ->
    s: LowParse.Spec.Base.serializer p1 ->
    u20: u21: Prims.unit{t2 == t1 /\ p2 == LowParse.Spec.Base.coerce_parser t2 p1}
  -> LowParse.Spec.Base.serializer p2
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer Prims.unit Prims.l_and Prims.eq2 LowParse.Spec.Base.coerce_parser
let coerce_parser_serializer
      (#t2: Type0)
      (#k: parser_kind)
      (#t1: Type0)
      (#p1: parser k t1)
      (p2: parser k t2)
      (s: serializer p1)
      (u: unit{t2 == t1 /\ p2 == coerce_parser t2 p1})
    : Tot (serializer (p2)) =
  
s