Function lemma_disjoint_and_then 

pub broadcast proof fn lemma_disjoint_and_then<U: SpecParser, Head: SpecParser<PVal = Seq<u8>>, Tail: SpecParser>(
    other: U,
    and_then: AndThen<Head, Tail>,
)

requires

disjoint_domains(other, and_then.0),

ensures

#[trigger] disjoint_domains(other, and_then),

An AndThen parser is disjoint from another parser if its byte-source parser is.