How does one prove theorems where the conclusion is an existentially quantified coinductive proposition?

I am attempting to adapt Xavier Leroy’s compiler correctness tutorial; this involves adding traces of events to the source and target languages. For the coinductive `infseq`

predicate, I have done this as follows:

```
(* the type of states *)
Variable A: Type.
Variable event: Type.
Variable R: A -> event -> A -> Prop.
Definition trace := list event.
Definition inftrace := Stream event.
Inductive star: A -> trace -> A -> Prop :=
| star_refl: forall a,
star a [] a
| star_step_ev: forall a b c e t,
R a e b -> star b t c -> star a (e :: t) c.
Definition all_seq_inf (a: A) : Prop :=
forall t b, star a t b -> exists e c, R b e c.
CoInductive infseq: A -> inftrace -> Prop :=
| infseq_step_ev: forall a e b t,
R a e b -> infseq b t -> infseq a (Cons e t).
```

I need to prove the following lemma:

```
Lemma infseq_if_all_seq_inf:
forall a, all_seq_inf a -> exists t, infseq a t.
```

However, I am unable to use `cofix`

on this goal–I get the error `All methods must construct elements in coinductive types.`

When traces are not involved, the equivalent lemma is fairly easy to prove (see here).

I would be really grateful for any suggestions on how to prove this.