Function arr_ext_append_size_ty 

pub fn arr_ext_append_size_ty() -> Expr

Array.append_size : ∀ {α n m}, Array α n → Array α m → Prop

Size of append equals sum: size (a ++ b) = size a + size b.