proposition: Theorem ForAll_EX_T : forall (Sini : S) (P : S -> Prop) (bound : Instant -> Prop), ForAll_T Sini P bound <-> ~ Exists_T Sini (fun s : S => ~ P s) bound.
proof: Proof. unfold not in |- *; unfold ForAll_T in |- *; red in |- *; intros; split; intros. inversion H0. apply (H3 (H s t H1 H2)). elim (classic (P s)); [ trivial | intro; absurd (Exists_T Sini (fun s : S => P s -> False) bound) ]. assumption. apply exists_T with (2 := H1); assumption. Qed.
imports: time_clocks Classical