Question: In Maple, how do I show two geometric regions (defined by some formulae) are equal?

Let us begin with few simulations: 
 

Download iDistributionVector.mws

Well, I'd like to prove (through the use of Maple): 

transform((x1, x2, x3, x4, x5) -> [x1 - x3, x2 - x4, x5])(inequal(And((x || (1 .. 5)) >=~ 0, norm([x || (1 .. 5)], 1) = 1))) # not Maple syntax

is equivalent to a filled pyramid

ImplicitRegion((X, Y, Z), 0 <= Z <= 1 - abs(X) - abs(Y)) # not SymPy syntax

, 

transform((x1, x2, x3, x4, x5) -> [x1 - x3, x2 - x4, x5])(inequal(And((x || (1 .. 5)) >=~ 0, norm([x || (1 .. 5)], 2) = 1))) # not Maple syntax

is equivalent to a hemi-ball

ImplicitRegion((X, Y, Z), 0 <= Z <= sqrt(1 - X**2 - Y**2)) # not SymPy syntax

, and 

transform((x1, x2, x3, x4, x5) -> [x1 - x3, x2 - x4, x5])(inequal(And((x || (1 .. 5)) >=~ 0, norm([x || (1 .. 5)], 'infinity') = 1))) # not Maple syntax

is equivalent to a solid cuboid

ImplicitRegion((X, Y, Z), -1 <= X <= 1 & -1 <= Y <= 1 & 0 <= Z <= 1) # not SymPy syntax

. (Here, for the convenience of the descriptions, I utilize some non-standard notation from sympy.vector.) 
Note that ”two regions are equal" is a two-way property, which means the following proof 

is(Z >= 0) and is(Z <= 1 - abs(X) - abs(Y)) assuming (X, Y, Z) =~ (x1 - x3, x2 - x4, x5), x || (1 .. 5) >=~ 0, add(x || (1 .. 5)) = 1;
                              true
(*Accordingly, the latter region is a subset of the former one.*) 

is incomplete (because it's hard to determine whether the is routine always performs equivalent transformations in internal evaluation). 

So, can I execute such eliminations in Maple?