proposition: Theorem Equiv1 : forall (Sini : S) (P : Stream S -> Prop), Posible Sini P <-> EX_Until Sini (fun _ : Stream S => True) P.
proof: Proof. unfold iff in |- *; intros; split; intro. inversion_clear H. apply ExUntil with (P := fun _ : Stream S => True) (1 := H0). elim H1; intros. constructor 2; assumption. constructor 1; trivial. inversion_clear H. apply posible with (1 := H0). elim H1; intros. constructor 2; assumption. constructor 1; assumption. Qed.
imports: Streams time_clocks