fact: Definition Inevitable_T (Sini : S * Instant) (P : Stream (S * Instant) -> Prop) := forall x : Stream (S * Instant), isTraceFrom_T Sini x -> ExistsS (fun s : Stream (S * Instant) => bound (snd (hd s)) /\ P s) x.
imports: time_clocks ctl