proposition: Lemma notPosible : forall (P : Stream S -> Prop) (s1 : S), ~ Posible s1 P -> forall (z : Stream S) (s2 : S), isTraceFrom s1 (s1 ^ s2 ^ z) -> ~ Posible s2 P.
proof: Proof. unfold not at 2 in |- *; intros. elim H1; intros. apply H; cut (isTraceFrom s1 (s1 ^ x)). intro H4; apply (posible (P:=P) H4). apply Further; assumption. apply ConsTrace with (1 := H2) (2 := H0); assumption. Qed.
imports: Streams time_clocks