proposition: Theorem Mon_I_S : forall (x : Stream S) (Pg Pp : Stream S -> Prop), ForAllS Pg x -> (forall s : Stream S, Pg s -> Pp s) -> ForAllS Pp x.
proof: Proof. cofix u; intro x; case x; intros. case H; constructor. apply (H0 (s1 ^ x0) H1). apply (u x0 Pg Pp H2 H0). Qed.
imports: Streams time_clocks Classical