Function arr_ext_map_id_ty 

pub fn arr_ext_map_id_ty() -> Expr

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

Functor identity law: mapping the identity function over an array returns the same array. map id a = a.