proposition: Theorem Mon_I_EX_S : forall (x : Stream S) (Pg Pp : Stream S -> Prop), ExistsS Pg x -> (forall s : Stream S, Pg s -> Pp s) -> ExistsS Pp x.
proof: Proof. simple induction 1; intros. constructor 1; apply (H1 x0 H0). constructor 2; apply (H1 H2). Qed.
imports: Streams time_clocks Classical