proposition: Theorem Conj_S : forall (x : Stream S) (P1 P2 : Stream S -> Prop), ForAllS P1 x -> ForAllS P2 x -> ForAllS (fun s : Stream S => P1 s /\ P2 s) x.
proof: Proof. cofix u; intro x; case x; intros. inversion_clear H; inversion_clear H0. constructor; [ split | apply (u s0) ]; assumption. Qed.
imports: Streams time_clocks Classical