proposition: Theorem Equiv2_T : forall (Sini : S * Instant) (P : Stream (S * Instant) -> Prop), Inevitable_T Sini P <-> FA_Until_bound Sini (fun _ : Stream (S * Instant) => True) P.
proof: Proof. unfold iff, Inevitable_T, FA_Until_bound in |- *; intros; split; intros. elim (H x H0); simple destruct x0. simple destruct p; intros. elim H1; intros. constructor 2; assumption. constructor 1; trivial. elim (H x H0); intros. constructor 2; assumption. constructor 1; split; assumption. Qed.
imports: time_clocks ctl