Function arr_ext_reverse_involution_ty 

pub fn arr_ext_reverse_involution_ty() -> Expr

Array.reverse_involution : ∀ {α n}, Array α n → Prop

Reversal is an involution: reverse (reverse a) = a.