Function extern_spec_T_U_Option__tuple2_T_U_unzip 

pub fn extern_spec_T_U_Option__tuple2_T_U_unzip<T, U>(
    self_: Option<(T, U)>,
) -> (Option<T>, Option<U>)

extern spec for Option<(T, U)>::unzip

This is not a real function: its only use is for documentation.

terminates

ghost

ensures

match self {
    None => result == (None, None),
    Some((t, u)) => result == (Some(t), Some(u)),
}