diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
index d900c8e9d4..85759acb60 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
@@ -129,7 +129,7 @@ specialization. Thus, the typevar is a subtype of itself and of `object`, but no
 (including other typevars).
 
 ```py
-from ty_extensions import is_assignable_to, is_subtype_of
+from ty_extensions import is_assignable_to, is_subtype_of, static_assert
 
 class Super: ...
 class Base(Super): ...
@@ -139,45 +139,83 @@ class Unrelated: ...
 def unbounded_unconstrained[T, U](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, T))
+    static_assert(is_assignable_to(T, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, object))
+    static_assert(is_assignable_to(T, object))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(T, Super))
+    static_assert(not is_assignable_to(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(U, U))
+    static_assert(is_assignable_to(U, U))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(U, object))
+    static_assert(is_assignable_to(U, object))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(U, Super))
+    static_assert(not is_assignable_to(U, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(T, U))
+    static_assert(not is_assignable_to(T, U))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(U, T))
+    static_assert(not is_assignable_to(U, T))
 
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_subtype_of(T, T))
+    static_assert(is_subtype_of(T, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_subtype_of(T, object))
+    static_assert(is_subtype_of(T, object))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_subtype_of(U, U))
+    static_assert(is_subtype_of(U, U))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_subtype_of(U, object))
+    static_assert(is_subtype_of(U, object))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(U, Super))
+    static_assert(not is_subtype_of(U, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, U))
+    static_assert(not is_subtype_of(T, U))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(U, T))
+    static_assert(not is_subtype_of(U, T))
 ```
 
 A bounded typevar is assignable to its bound, and a bounded, fully static typevar is a subtype of
@@ -193,56 +231,100 @@ from typing_extensions import final
 def bounded[T: Super](t: T) -> None:
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded ≤ Super)]
     reveal_type(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded ≤ Super)]
     reveal_type(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded ≤ Super)]
     reveal_type(is_assignable_to(T, Super))
+    static_assert(is_assignable_to(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Super, T))
+    static_assert(not is_assignable_to(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Sub, T))
+    static_assert(not is_assignable_to(Sub, T))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded ≤ Super)]
     reveal_type(is_subtype_of(T, Super))
+    static_assert(is_subtype_of(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Sub, T))
+    static_assert(not is_subtype_of(Sub, T))
 
 def bounded_by_gradual[T: Any](t: T) -> None:
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Super))
+    static_assert(is_assignable_to(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Super, T))
+    static_assert(not is_assignable_to(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Sub))
+    static_assert(is_assignable_to(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Sub, T))
+    static_assert(not is_assignable_to(Sub, T))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Sub, T))
+    static_assert(not is_subtype_of(Sub, T))
 
 @final
 class FinalClass: ...
@@ -250,21 +332,35 @@ class FinalClass: ...
 def bounded_final[T: FinalClass](t: T) -> None:
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded_final ≤ FinalClass)]
     reveal_type(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded_final ≤ FinalClass)]
     reveal_type(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded_final ≤ FinalClass)]
     reveal_type(is_assignable_to(T, FinalClass))
+    static_assert(is_assignable_to(T, FinalClass))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(FinalClass, T))
+    static_assert(not is_assignable_to(FinalClass, T))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@bounded_final ≤ FinalClass)]
     reveal_type(is_subtype_of(T, FinalClass))
+    static_assert(is_subtype_of(T, FinalClass))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(FinalClass, T))
+    static_assert(not is_subtype_of(FinalClass, T))
 ```
 
 Two distinct fully static typevars are not subtypes of each other, even if they have the same
@@ -276,24 +372,36 @@ typevars to `Never` in addition to that final class.
 def two_bounded[T: Super, U: Super](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(T, U))
+    static_assert(not is_assignable_to(T, U))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(U, T))
+    static_assert(not is_assignable_to(U, T))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, U))
+    static_assert(not is_subtype_of(T, U))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(U, T))
+    static_assert(not is_subtype_of(U, T))
 
 def two_final_bounded[T: FinalClass, U: FinalClass](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(T, U))
+    static_assert(not is_assignable_to(T, U))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(U, T))
+    static_assert(not is_assignable_to(U, T))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, U))
+    static_assert(not is_subtype_of(T, U))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(U, T))
+    static_assert(not is_subtype_of(U, T))
 ```
 
 A constrained fully static typevar is assignable to the union of its constraints, but not to any of
@@ -306,124 +414,236 @@ from ty_extensions import Intersection
 def constrained[T: (Base, Unrelated)](t: T) -> None:
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
     reveal_type(is_assignable_to(T, Super))
+    static_assert(not is_assignable_to(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
     reveal_type(is_assignable_to(T, Base))
+    static_assert(not is_assignable_to(T, Base))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(T, Unrelated))
+    static_assert(not is_assignable_to(T, Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(T, Super | Unrelated))
+    static_assert(is_assignable_to(T, Super | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(T, Base | Unrelated))
+    static_assert(is_assignable_to(T, Base | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(T, Sub | Unrelated))
+    static_assert(not is_assignable_to(T, Sub | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Super, T))
+    static_assert(not is_assignable_to(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(Unrelated, T))
+    static_assert(not is_assignable_to(Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_assignable_to(Super | Unrelated, T))
+    static_assert(not is_assignable_to(Super | Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))
+    static_assert(is_assignable_to(Intersection[Base, Unrelated], T))
 
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
     reveal_type(is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Base)]
     reveal_type(is_subtype_of(T, Base))
+    static_assert(not is_subtype_of(T, Base))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
     reveal_type(is_subtype_of(T, Unrelated))
+    static_assert(not is_subtype_of(T, Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_subtype_of(T, Super | Unrelated))
+    static_assert(is_subtype_of(T, Super | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_subtype_of(T, Base | Unrelated))
+    static_assert(is_subtype_of(T, Base | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
     reveal_type(is_subtype_of(T, Sub | Unrelated))
+    static_assert(not is_subtype_of(T, Sub | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained = Unrelated)]
     reveal_type(is_subtype_of(Unrelated, T))
+    static_assert(not is_subtype_of(Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super | Unrelated, T))
+    static_assert(not is_subtype_of(Super | Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@constrained = Base) ∨ (T@constrained = Unrelated)]
     reveal_type(is_subtype_of(Intersection[Base, Unrelated], T))
+    static_assert(is_subtype_of(Intersection[Base, Unrelated], T))
 
 def constrained_by_gradual[T: (Base, Any)](t: T) -> None:
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Super))
+    static_assert(is_assignable_to(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Base))
+    static_assert(is_assignable_to(T, Base))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
     reveal_type(is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
     reveal_type(is_assignable_to(T, Unrelated))
+    static_assert(not is_assignable_to(T, Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Super | Any))
+    static_assert(is_assignable_to(T, Super | Any))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(T, Super | Unrelated))
+    static_assert(is_assignable_to(T, Super | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
     reveal_type(is_assignable_to(Super, T))
+    static_assert(not is_assignable_to(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Base, T))
+    static_assert(is_assignable_to(Base, T))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
     reveal_type(is_assignable_to(Unrelated, T))
+    static_assert(not is_assignable_to(Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
     reveal_type(is_assignable_to(Super | Any, T))
+    static_assert(not is_assignable_to(Super | Any, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Base | Any, T))
+    static_assert(is_assignable_to(Base | Any, T))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: (T@constrained_by_gradual ≠ Base)]
     reveal_type(is_assignable_to(Super | Unrelated, T))
+    static_assert(not is_assignable_to(Super | Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))
+    static_assert(is_assignable_to(Intersection[Base, Unrelated], T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Intersection[Base, Any], T))
+    static_assert(is_assignable_to(Intersection[Base, Any], T))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Super))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Base))
+    static_assert(not is_subtype_of(T, Base))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(T, Sub))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Unrelated))
+    static_assert(not is_subtype_of(T, Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Super | Any))
+    static_assert(not is_subtype_of(T, Super | Any))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T, Super | Unrelated))
+    static_assert(not is_subtype_of(T, Super | Unrelated))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Super, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Base, T))
+    static_assert(not is_subtype_of(Base, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Unrelated, T))
+    static_assert(not is_subtype_of(Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super | Any, T))
+    static_assert(not is_subtype_of(Super | Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Base | Any, T))
+    static_assert(not is_subtype_of(Base | Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Super | Unrelated, T))
+    static_assert(not is_subtype_of(Super | Unrelated, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Intersection[Base, Unrelated], T))
+    static_assert(not is_subtype_of(Intersection[Base, Unrelated], T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(Intersection[Base, Any], T))
+    static_assert(not is_subtype_of(Intersection[Base, Any], T))
 ```
 
 Two distinct fully static typevars are not subtypes of each other, even if they have the same
@@ -435,13 +655,19 @@ the same type.
 def two_constrained[T: (int, str), U: (int, str)](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_constrained = str) ∧ (U@two_constrained = str)) ∨ ((T@two_constrained = int) ∧ (U@two_constrained = int))]
     reveal_type(is_assignable_to(T, U))
+    static_assert(not is_assignable_to(T, U))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_constrained = str) ∧ (T@two_constrained = str)) ∨ ((U@two_constrained = int) ∧ (T@two_constrained = int))]
     reveal_type(is_assignable_to(U, T))
+    static_assert(not is_assignable_to(U, T))
 
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_constrained = str) ∧ (U@two_constrained = str)) ∨ ((T@two_constrained = int) ∧ (U@two_constrained = int))]
     reveal_type(is_subtype_of(T, U))
+    static_assert(not is_subtype_of(T, U))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_constrained = str) ∧ (T@two_constrained = str)) ∨ ((U@two_constrained = int) ∧ (T@two_constrained = int))]
     reveal_type(is_subtype_of(U, T))
+    static_assert(not is_subtype_of(U, T))
 
 @final
 class AnotherFinalClass: ...
@@ -449,13 +675,19 @@ class AnotherFinalClass: ...
 def two_final_constrained[T: (FinalClass, AnotherFinalClass), U: (FinalClass, AnotherFinalClass)](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_final_constrained = AnotherFinalClass) ∧ (U@two_final_constrained = AnotherFinalClass)) ∨ ((T@two_final_constrained = FinalClass) ∧ (U@two_final_constrained = FinalClass))]
     reveal_type(is_assignable_to(T, U))
+    static_assert(not is_assignable_to(T, U))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_final_constrained = AnotherFinalClass) ∧ (T@two_final_constrained = AnotherFinalClass)) ∨ ((U@two_final_constrained = FinalClass) ∧ (T@two_final_constrained = FinalClass))]
     reveal_type(is_assignable_to(U, T))
+    static_assert(not is_assignable_to(U, T))
 
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((T@two_final_constrained = AnotherFinalClass) ∧ (U@two_final_constrained = AnotherFinalClass)) ∨ ((T@two_final_constrained = FinalClass) ∧ (U@two_final_constrained = FinalClass))]
     reveal_type(is_subtype_of(T, U))
+    static_assert(not is_subtype_of(T, U))
+
     # revealed: ty_extensions.ConstraintSet[some valid specializations: ((U@two_final_constrained = AnotherFinalClass) ∧ (T@two_final_constrained = AnotherFinalClass)) ∨ ((U@two_final_constrained = FinalClass) ∧ (T@two_final_constrained = FinalClass))]
     reveal_type(is_subtype_of(U, T))
+    static_assert(not is_subtype_of(U, T))
 ```
 
 A bound or constrained typevar is a subtype of itself in a union:
@@ -464,13 +696,19 @@ A bound or constrained typevar is a subtype of itself in a union:
 def union[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@union ≤ Base)]
     reveal_type(is_assignable_to(T, T | None))
+    static_assert(is_assignable_to(T, T | None))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@union = Base) ∨ (U@union = Unrelated)]
     reveal_type(is_assignable_to(U, U | None))
+    static_assert(is_assignable_to(U, U | None))
 
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@union ≤ Base)]
     reveal_type(is_subtype_of(T, T | None))
+    static_assert(is_subtype_of(T, T | None))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@union = Base) ∨ (U@union = Unrelated)]
     reveal_type(is_subtype_of(U, U | None))
+    static_assert(is_subtype_of(U, U | None))
 ```
 
 A bound or constrained typevar in a union with a dynamic type is assignable to the typevar:
@@ -479,32 +717,44 @@ A bound or constrained typevar in a union with a dynamic type is assignable to t
 def union_with_dynamic[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@union_with_dynamic ≤ Base)]
     reveal_type(is_assignable_to(T | Any, T))
+    static_assert(is_assignable_to(T | Any, T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@union_with_dynamic = Base) ∨ (U@union_with_dynamic = Unrelated)]
     reveal_type(is_assignable_to(U | Any, U))
+    static_assert(is_assignable_to(U | Any, U))
 
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(T | Any, T))
+    static_assert(not is_subtype_of(T | Any, T))
+
     # revealed: ty_extensions.ConstraintSet[never]
     reveal_type(is_subtype_of(U | Any, U))
+    static_assert(not is_subtype_of(U | Any, U))
 ```
 
 And an intersection of a typevar with another type is always a subtype of the TypeVar:
 
 ```py
-from ty_extensions import Intersection, Not, is_disjoint_from, static_assert
+from ty_extensions import Intersection, Not, is_disjoint_from
 
 class A: ...
 
 def inter[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@inter ≤ Base)]
     reveal_type(is_assignable_to(Intersection[T, Unrelated], T))
+    static_assert(is_assignable_to(Intersection[T, Unrelated], T))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (T@inter ≤ Base)]
     reveal_type(is_subtype_of(Intersection[T, Unrelated], T))
+    static_assert(is_subtype_of(Intersection[T, Unrelated], T))
 
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@inter = Base) ∨ (U@inter = Unrelated)]
     reveal_type(is_assignable_to(Intersection[U, A], U))
+    static_assert(is_assignable_to(Intersection[U, A], U))
+
     # revealed: ty_extensions.ConstraintSet[all valid specializations: (U@inter = Base) ∨ (U@inter = Unrelated)]
     reveal_type(is_subtype_of(Intersection[U, A], U))
+    static_assert(is_subtype_of(Intersection[U, A], U))
 
     static_assert(is_disjoint_from(Not[T], T))
     static_assert(is_disjoint_from(T, Not[T]))
@@ -801,18 +1051,24 @@ The intersection of a typevar with any other type is assignable to (and if fully
 of) itself.
 
 ```py
-from ty_extensions import is_assignable_to, is_subtype_of, Not
+from ty_extensions import is_assignable_to, is_subtype_of, Not, static_assert
 
 def intersection_is_assignable[T](t: T) -> None:
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Intersection[T, None], T))
+    static_assert(is_assignable_to(Intersection[T, None], T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_assignable_to(Intersection[T, Not[None]], T))
+    static_assert(is_assignable_to(Intersection[T, Not[None]], T))
 
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_subtype_of(Intersection[T, None], T))
+    static_assert(is_subtype_of(Intersection[T, None], T))
+
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(is_subtype_of(Intersection[T, Not[None]], T))
+    static_assert(is_subtype_of(Intersection[T, Not[None]], T))
 ```
 
 ## Narrowing