proposition: Theorem Mon_I_EX_T : forall (Sini : S) (Pg Pp : S -> Prop) (bound : Instant -> Prop), Exists_T Sini Pg bound -> (forall s : S, Pg s -> Pp s) -> Exists_T Sini Pp bound.
proof: Proof. intros. inversion_clear H. apply (exists_T H1 H2 (H0 s H3)). Qed.
imports: time_clocks