diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md
index 20dcce4..08eb341 100644
--- a/4a1s/MFES/PL - Aula 5.md	
+++ b/4a1s/MFES/PL - Aula 5.md	
@@ -51,7 +51,7 @@ pred Invs {
     //keys are unique to a single node
   	all k: Key | one x: Node | x.key = k
 
-    //heads are unique to a single bucket
+    //heads are unique to a single bucket (UNNECESSARY)
   	all x: Bucket | lone x.head
   
   	//nodes must be prox to another node or be the head of a bucket
@@ -62,6 +62,9 @@ pred Invs {
   
   	//keys must have a hash
   	all x: Key | some y: Hash | x.hash = y
+  	
+  	//nodes(heads) associated to different buckets, must differ in hash
+  	all x, y: Bucket | (x != y and x.head != none and y.head != none ) implies x.head.key.hash != y.head.key.hash
 
 }