let n = 3
node ok_since_n_instants(b:bool) returns (res:bool) =
  exist cpt: int = n in 
     loop { 
       cpt = (if b then (pre cpt-1) else n) and 
       res = (b and (cpt <= 0)) 
     }