proposition: Theorem ForAll_EX : forall (Sini : S) (P : S -> Prop), ForAll Sini P <-> ~ Exists Sini (fun s : S => ~ P s).
proof: Proof. unfold not in |- *; unfold ForAll in |- *; red in |- *; intros; split; intros. inversion H0. apply (H2 (H s H1)). elim (classic (P s)); [ trivial | intro; absurd (Exists Sini (fun s : S => P s -> False)) ]. assumption. apply exists_ with (1 := H0); assumption. Qed.
imports: time_clocks Classical