Function arr_ext_append_empty_right_ty 

pub fn arr_ext_append_empty_right_ty() -> Expr

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

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