proposition: Theorem Mon_I_EX : forall (Sini : S) (Pg Pp : S -> Prop), Exists Sini Pg -> (forall s : S, Pg s -> Pp s) -> Exists Sini Pp.
proof: Proof. intros. inversion_clear H. apply (exists_ H1 (H0 s H2)). Qed.
imports: time_clocks