diff --git a/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
index 0879592d3c..6aed38694a 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
@@ -663,6 +663,7 @@ to the fact that `bool` is a `@final` class at runtime that cannot be subclassed
 
 ```py
 from knot_extensions import Intersection, Not, AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Literal
 
 class P: ...
 
@@ -686,6 +687,19 @@ def f(
     reveal_type(f)  # revealed: Never
     reveal_type(g)  # revealed: Never
     reveal_type(h)  # revealed: Never
+
+def never(
+    a: Intersection[Intersection[AlwaysFalsy, Not[Literal[False]]], bool],
+    b: Intersection[Intersection[AlwaysTruthy, Not[Literal[True]]], bool],
+    c: Intersection[Intersection[Literal[True], Not[AlwaysTruthy]], bool],
+    d: Intersection[Intersection[Literal[False], Not[AlwaysFalsy]], bool],
+):
+    # TODO: This should be `Never`
+    reveal_type(a)  # revealed: Literal[True]
+    # TODO: This should be `Never`
+    reveal_type(b)  # revealed: Literal[False]
+    reveal_type(c)  # revealed: Never
+    reveal_type(d)  # revealed: Never
 ```
 
 ## Simplification of `LiteralString`, `AlwaysTruthy` and `AlwaysFalsy`
diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
index 54c313f789..05eacd07c3 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
@@ -206,8 +206,8 @@ static_assert(not is_assignable_to(tuple[Any, Literal[2]], tuple[int, str]))
 ## Union types
 
 ```py
-from knot_extensions import static_assert, is_assignable_to, Unknown
-from typing import Literal, Any
+from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_assignable_to, Unknown
+from typing_extensions import Literal, Any, LiteralString
 
 static_assert(is_assignable_to(int, int | str))
 static_assert(is_assignable_to(str, int | str))
@@ -227,13 +227,22 @@ static_assert(not is_assignable_to(int | None, str | None))
 static_assert(not is_assignable_to(Literal[1] | None, int))
 static_assert(not is_assignable_to(Literal[1] | None, str | None))
 static_assert(not is_assignable_to(Any | int | str, int))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_assignable_to(bool, Literal[False] | AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_assignable_to(bool, Literal[True] | AlwaysFalsy))
+# error: [static-assert-error]
+static_assert(is_assignable_to(LiteralString, Literal[""] | AlwaysTruthy))
+static_assert(not is_assignable_to(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy))
 ```
 
 ## Intersection types
 
 ```py
-from knot_extensions import static_assert, is_assignable_to, Intersection, Not
-from typing_extensions import Any, Literal
+from knot_extensions import static_assert, is_assignable_to, Intersection, Not, AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Any, Literal, final, LiteralString
 
 class Parent: ...
 class Child1(Parent): ...
@@ -296,6 +305,19 @@ static_assert(is_assignable_to(Intersection[Any, Unrelated], Intersection[Any, P
 static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Intersection[Any, Parent, Unrelated]))
 static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Not[Any]]))
 static_assert(is_assignable_to(Intersection[Literal[1], Any], Intersection[Unrelated, Not[Any]]))
+
+# TODO: No errors
+# The condition `is_assignable_to(T & U, U)` should still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy]))
+# error: [static-assert-error]
+static_assert(is_assignable_to(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
 ```
 
 ## General properties
diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index 9a600816fa..3d2296807d 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
@@ -196,7 +196,7 @@ static_assert(is_disjoint_from(None, Intersection[int, Not[str]]))
 
 ```py
 from typing_extensions import Literal, LiteralString
-from knot_extensions import TypeOf, is_disjoint_from, static_assert
+from knot_extensions import Intersection, Not, TypeOf, is_disjoint_from, static_assert, AlwaysFalsy, AlwaysTruthy
 
 static_assert(is_disjoint_from(Literal[True], Literal[False]))
 static_assert(is_disjoint_from(Literal[True], Literal[1]))
@@ -223,6 +223,25 @@ static_assert(not is_disjoint_from(Literal[1], Literal[1]))
 static_assert(not is_disjoint_from(Literal["a"], Literal["a"]))
 static_assert(not is_disjoint_from(Literal["a"], LiteralString))
 static_assert(not is_disjoint_from(Literal["a"], str))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_disjoint_from(AlwaysFalsy, Intersection[LiteralString, Not[Literal[""]]]))
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[Not[Literal[True]], Not[Literal[False]]], bool))
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[AlwaysFalsy, Not[Literal[False]]], bool))
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[AlwaysTruthy, Not[Literal[True]]], bool))
+
+# TODO: No errors
+# The condition `is_disjoint(T, Not[T])` must still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[LiteralString, AlwaysTruthy], Not[LiteralString] | AlwaysFalsy))
+# `LiteralString & ~AlwaysFalsy`  -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_disjoint_from(Intersection[LiteralString, Not[AlwaysFalsy]], Not[LiteralString] | AlwaysFalsy))
 ```
 
 ### Class, module and function literals
diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md
index a559e93181..fce0395bde 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md
@@ -46,6 +46,12 @@ static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]],
 
 static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes))
 static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_gradual_equivalent_to(Unknown, Unknown | Any))
+# error: [static-assert-error]
+static_assert(is_gradual_equivalent_to(Unknown, Intersection[Unknown, Any]))
 ```
 
 ## Tuples
diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
index 3998c0a0f1..9eb0165451 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
@@ -276,8 +276,8 @@ static_assert(is_subtype_of(Never, AlwaysFalsy))
 ### `AlwaysTruthy` and `AlwaysFalsy`
 
 ```py
-from knot_extensions import AlwaysTruthy, AlwaysFalsy, is_subtype_of, static_assert
-from typing import Literal
+from knot_extensions import AlwaysTruthy, AlwaysFalsy, Intersection, Not, is_subtype_of, static_assert
+from typing_extensions import Literal, LiteralString
 
 static_assert(is_subtype_of(Literal[1], AlwaysTruthy))
 static_assert(is_subtype_of(Literal[0], AlwaysFalsy))
@@ -290,6 +290,28 @@ static_assert(not is_subtype_of(Literal[0], AlwaysTruthy))
 
 static_assert(not is_subtype_of(str, AlwaysTruthy))
 static_assert(not is_subtype_of(str, AlwaysFalsy))
+
+# TODO: No errors
+# error: [static-assert-error]
+static_assert(is_subtype_of(bool, Literal[False] | AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_subtype_of(bool, Literal[True] | AlwaysFalsy))
+# error: [static-assert-error]
+static_assert(is_subtype_of(LiteralString, Literal[""] | AlwaysTruthy))
+static_assert(not is_subtype_of(Literal[True] | AlwaysFalsy, Literal[False] | AlwaysTruthy))
+
+# TODO: No errors
+# The condition `is_subtype_of(T & U, U)` must still be satisfied after the following transformations:
+# `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], AlwaysTruthy))
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], AlwaysTruthy))
+# `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]`
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal[""]]], Not[AlwaysFalsy]))
+# error: [static-assert-error]
+static_assert(is_subtype_of(Intersection[LiteralString, Not[Literal["", "a"]]], Not[AlwaysFalsy]))
 ```
 
 ### Module literals