Function array_option_unwrap 

pub exec fn array_option_unwrap<T: DeepView, const N: usize>(
    arr: [Option<T>; N],
) -> out : [T; N]

requires

forall |j: int| 0 <= j < N ==> #[trigger] arr@[j] is Some,

ensures

out.deep_view() == Seq::new(N as nat, |j| arr@[j]->0.deep_view()),