proposition: Lemma not_EX : forall (P : Stream S -> Prop) (x : Stream S) (s : S), ~ ExistsS P (s ^ x) -> ~ ExistsS P x.
proof: Proof. unfold not in |- *; intros. apply (H (Further s H0)). Qed.
imports: Streams time_clocks Classical