Function disjoint_values 

pub open spec fn disjoint_values<C1, C2>(c1: C1, c2: C2) -> bool
where
    C1: Consistency,
    C2: Consistency<Val = C1::Val>,

{ forall |v: C1::Val| c1.consistent(v) && c2.consistent(v) ==> false }

Combinator denotations that admit disjoint (mutually exclusive) sets of consistent values.

Used by crate::combinators::Alt to recover non-malleability.