How to prove by coinduction?

Question

Previously, I've asked a question about coinduction. That gave me a lot of useful high-level insights on what coinduction provides, and what are the usefulness of coinductive proofs.

This question is about walking through an example in more detail. The example is based on this other question "What is coinduction?". I'll copy some Coq code from that question over here.

First, we have a colist.

CoInductive colist (A:Set) : Set :=
  | conil : colist A
  | cocons : A -> colist A -> colist A.

Then we have the from function.

CoFixpoint from (n:Nat) : colist Nat := cocons n (from (1 + n)).

Then we have a proposition about infinite colists.

CoInductive Infinite A : colist A -> Prop :=
  | Inf : forall x l, Infinite l -> Infinite (cocons x l).

I'd like to prove forall n, Infinite from n.

Using The coinduction principle [1] says to prove $X \subseteq vF$, it suffices to show $X \subseteq F X$.

Questions: What is $X$, $F$, $vF$, the theorem $X \subseteq vF$, and the proof obligation $X \subseteq F X$ stated in terms of from and Infinite?

---

Below is my attempt to answer these questions.

$X$ is the set of colists "generated by" from. Maybe it looks like this?

x: Nat    from (x+1): ColistGeneratedByFrom
-------------------------------------------
cocons x from (x+1): ColistGeneratedByFrom

$F$ is applying Infinite once.

F(X) = {cocons x l | x: Nat, l: X}

$vF$ is the set of colists "generated by" Infinite. Maybe it looks like this?

y: Nat   l: ColistGeneratedByInfinite
-------------------------------------
cocons y l: ColistGeneratedByInfinite

The theorem $X \subseteq vF$ is proving that ColistGeneratedByFrom $\subseteq$ ColistGeneratedByInfinite. That any colist generated by from has the property Infinite.

The proof obligation $X \subseteq F X$ says that we only need to show that a colist generated by from is "survives" applying Infinite once.

From [1], I think that I would need to show something like.

forall n: Nat,
  exists m: ColistGeneratedByFrom,
    x: ColistGeneratedByFrom => x = cocons n m

But I'm confused how does $F$ lead to this principle that uses exists.

I would have simply tried to applied $F$ and get something like

forall n: Nat,
  x: ColistGeneratedByFrom => cocons n x: ColistGeneratedByFrom

which I'm not sure can be proven.

Where is my understanding correct / incorrect?

Apologies if I'm mixing notations.

[1] Programming = proving? The Curry-Howard correspondence today