Function lemma_disjoint_asn1_starts 

pub broadcast proof fn lemma_disjoint_asn1_starts<Left: HasAsn1Start, Right: HasAsn1Start>(
    left: Left,
    right: Right,
)

requires

asn1_starts_disjoint(left.asn1_start(), right.asn1_start()),

ensures

#[trigger] disjoint_domains(left, right),

Key lemma: Disjoint ASN.1 start domains imply disjoint parser domains.

The theorem remains directly callable so generated code need not depend on quantifier-trigger discovery. Its single directional trigger is also useful for small hand-written formats.