Function arr_ext_map_comp_ty 

pub fn arr_ext_map_comp_ty() -> Expr

Array.map_comp : ∀ {α β γ n}, (β → γ) → (α → β) → Array α n → Prop

Functor composition law: mapping (g ∘ f) over an array equals mapping g after mapping f. map (g ∘ f) a = map g (map f a).