proposition: Theorem Conj_T : forall (Sini : S) (P1 P2 : S -> Prop) (bound : Instant -> Prop), ForAll_T Sini P1 bound -> ForAll_T Sini P2 bound -> ForAll_T Sini (fun s : S => P1 s /\ P2 s) bound.
proof: Proof. unfold ForAll_T in |- *; intros. split; [ apply (H s t) | apply (H0 s t) ]; assumption. Qed.
imports: time_clocks