Function lemma_disjoint_terminated_left 

pub broadcast proof fn lemma_disjoint_terminated_left<U1: SpecParser, V1: SpecParser, U: SpecParser, const CHECK: bool>(
    terminated: Terminated<U1, V1, V1::PVal, CHECK>,
    other: U,
)

requires

disjoint_domains(terminated.a, other),

ensures

#[trigger] disjoint_domains(terminated, other),

A Terminated parser is disjoint from another parser if its content parser is.