Function lemma_input_starts_with_union 

pub proof fn lemma_input_starts_with_union(
    input: Seq<u8>,
    left: Asn1StartDomain,
    right: Asn1StartDomain,
)

requires

input_starts_with(input, left) || input_starts_with(input, right),

ensures

input_starts_with(input, asn1_start_union(left, right)),