Function arr_ext_append_empty_left_ty 

pub fn arr_ext_append_empty_left_ty() -> Expr

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

Left identity of append: empty ++ a = a.