Function arbitrary_or_left 

pub open spec fn arbitrary_or_left(l: bool, r: bool) -> bool

{
    use vstd::pervasive::arbitrary;
    if l && r { arbitrary() } else { l }
}