Function input_starts_with 

pub open spec fn input_starts_with(input: Seq<u8>, domain: Asn1StartDomain) -> bool

{
    ||| input.len() == 0 && domain.accepts_empty
    ||| match TagFmt.spec_parse(input) {
        Some((_n, tag)) => tag_lead_mask_contains(domain.tags, tag),
        None => false,
    }

}

Whether input has a start represented by domain.