diff --git a/README.md b/README.md
index 1472b6f..a8ccb8a 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,6 @@ Our axioms are:
 Section Variables:
 side : HSet
 Axioms:
-STrue relies on definitional UIP. (* bug: coq/coq#16427 *)
 functional_extensionality_dep
   : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
 	(forall x : A, f x = g x) -> f = g