proposition: Lemma ConsTrace : forall (s1 s2 : S) (x z : Stream S), isTraceFrom s2 z -> isTraceFrom s1 (s1 ^ s2 ^ x) -> isTraceFrom s1 (s1 ^ z).
proof: Proof. unfold isTraceFrom in |- *; simpl in |- *. simple destruct z; simple destruct 1; simple destruct 3; simpl in |- *; intros. compute in H0; rewrite H0 in H4. inversion_clear H4 in H1. split; [ trivial | apply (isTraceTick H5 H1) ]. split; [ trivial | apply (isTraceDisc H5 H6 H1) ]. Qed.
imports: Streams time_clocks