proposition: Theorem Equiv2 : forall (Sini : S) (P : Stream S -> Prop), Inevitable Sini P <-> FA_Until Sini (fun _ : Stream S => True) P.
proof: Proof. unfold iff, Inevitable, FA_Until in |- *; intros; split; intros. elim (H x H0); intros. constructor 2; assumption. constructor 1; trivial. elim (H x H0); intros. constructor 2; assumption. constructor 1; assumption. Qed.
imports: Streams time_clocks