pub fn arr_ext_sort_perm_ty() -> Expr
Array.sort_perm : ∀ {α n}, [Ord α] → Array α n → Prop
Correctness of sort as a permutation: the sorted result is a permutation of the input (no elements added or dropped).