Function array_of_none 

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

ensures

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