Function bool_value_le_option_tokenCopy item path

pub open spec fn bool_value_le_option_token<Token: SimpleToken>(
    b: bool,
    opt_token: Option<Token>,
    instance_id: InstanceId,
) -> bool

{ b ==> opt_token.is_some() && opt_token.unwrap().instance_id() == instance_id }