proposition: Lemma notPosible_T : forall (P : Stream (S * Instant) -> Prop) (s1 : S * Instant), ~ Posible_T s1 P -> forall (z : Stream (S * Instant)) (s2 : S * Instant), isTraceFrom_T s1 (s1 ^ s2 ^ z) -> ~ Posible_T s2 P.
proof: Proof. unfold not at 2 in |- *; intros. elim H1; intros. apply H; cut (isTraceFrom_T s1 (s1 ^ x)). intro H4; apply (posible_T (P:=P) H4). apply Further; assumption. apply ConsTrace_T with (1 := H2) (2 := H0); assumption. Qed.
imports: time_clocks ctl