Function lemma_disjoint_and_then_left 

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

requires

disjoint_domains(and_then.0, other),

ensures

#[trigger] disjoint_domains(and_then, other),

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