diff --git a/4a1s/MFES/PL - Aula 7.md b/4a1s/MFES/PL - Aula 7.md
index ffde529..29f10f6 100644
--- a/4a1s/MFES/PL - Aula 7.md	
+++ b/4a1s/MFES/PL - Aula 7.md	
@@ -58,13 +58,10 @@ pred insert[n : Node] {
 pred insert[n : Node] {
   	//nodes always in the head or linked to prox
   	//always n in ( Bucket.head + Bucket.head.prox)
-  	always{
-      n in Bucket.head
+  	always n.key.hash not in Hash {
+	  	
   	}
   
-  	historically n.key.hash not in Hash
-  	lone b:Bucket | b.head = none implies b.head' = n
-  
 
 }