proposition: Theorem Mon_I_T : forall (Sini : S) (Pg Pp : S -> Prop) (bound : Instant -> Prop), ForAll_T Sini Pg bound -> (forall s : S, Pg s -> Pp s) -> ForAll_T Sini Pp bound.
proof: Proof. unfold ForAll_T in |- *; intros. apply H0. apply (H s t); assumption. Qed.
imports: time_clocks