Function spec_expectCopy item path

pub open spec fn spec_expect<T>(option: Option<T>, msg: &str) -> T

option is Some,

{ option->0 }