Function lemma_disjoint_cond 

pub broadcast proof fn lemma_disjoint_cond<Inner1: SpecParser, Inner2: SpecParser>(
    c1: Cond<Inner1>,
    c2: Cond<Inner2>,
)

requires

c1.0 && c2.0 ==> false,

ensures

#[trigger] disjoint_domains(c1, c2),

Two Cond parsers with mutually exclusive conditions are disjoint.