 then
                Result := b = Void
            else
                Result := b /= Void and then a.is_deep_equal (b)
            end
        ensure
            shallow_implies_deep: standard_equal (a, b) implies Result
            both_or_none_void: (a = Void) implies (Result = (b = Void))
            same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b))
            symmetric: Result implies deep_equal (b, a)
        end

feature -- Duplication

    frozen twin