A little bit of cleaning

theories/simulation/behavior.v

@@ -136,10 +136,6 @@ Section beh.
       stuck_pool p T σ →
       t ≈ ub -> has_beh p T σ t
   | HasBehDiv T σ t :
-    (* IY: itrees don't particularly capture a notion of fairness, but the
-      divergence predicate can be encoded .. *)
-    (* This constructor may contain trees that have undefined behavior.
-      How does this work w.r.t. fairness? (Also, does UB contain divergence?) *)
     fair_div p T σ → has_divergence t -> has_beh p T σ t
   | HasBehRet v T σ t:
       t ≈ Ret v ->