Nested inductive coinductive types don't seem to go through for induction principles. See https://www.joachim-breitner.de/blog/727-How_is_coinduction_the_dual_of_induction_ for induction/coinduciton using relators.

broken.agda

{-# OPTIONS --guardedness #-}
module ord where

record stream (A : Set) : Set where
  coinductive
  constructor _::_
  field
    head : A
    tail : stream A

record Forall {A : Set} (P : A → Set) (x : stream A) : Set where
  coinductive
  constructor _:>_
  field
    forhead : P (stream.head x)
    fortail : Forall P (stream.tail x)

data ord : Set where
  o : ord
  s : ord → ord
  sup : stream ord → ord

open stream
open Forall

ind : (P : ord → Set) → P o → ((x : ord) → P x → P (s x)) → ((x : stream ord) → Forall P x → P (sup x)) → (x : ord) → P x
ind P onO onS onSup = loop where
  loop : (x : ord) → P x
  loop o = onO
  loop (s x) = onS x (loop x)
  loop (sup x) = onSup x (gen x) where
    gen : (y : stream ord) → Forall P y
    forhead (gen y) = loop (head y)
    fortail (gen y) = gen (tail y)

broken.v

Global Set Universe Polymorphism.
Global Set Polymorphic Inductive Cumulativity.
Global Set Primitive Projections.

Import IfNotations.

CoInductive stream A := cons { head: A; tail: stream A }.

Arguments cons {A}.
Arguments head {A}.
Arguments tail {A}.

Infix ":>" := cons (at level 30).

Fixpoint nth {A} (s: stream A) (n: nat) :=
  match n with
  | O => head s
  | S n => nth (tail s) n
  end.

CoFixpoint seq {A} (p: nat -> A): stream A :=
  p O :> seq (fun n => p (S n)).

CoInductive map {A B} (P: A -> B -> Type) (x: stream A) (y: stream B) := {
    map_head: P (head x) (head y) ;
    map_tail: map P (tail x) (tail y) ;
}.

CoFixpoint stream_prod {A} {R P}:
  (forall (x y: stream A), P x y -> R (head x) (head y)) ->
  (forall (x y: stream A), P x y -> P (tail x) (tail y)) ->
  forall (x y: stream A), P x y -> map R x y.
Proof.
  intros onHead onTail.
  intros ? ?.
  exists.
  - apply onHead.
    auto.
  - apply (stream_prod _ _ _ onHead onTail).
    apply onTail.
    auto.
Defined.

Inductive ord := O | S (n: ord) | Sup (s: stream ord).

Inductive eq: ord -> ord -> Type :=
| eq_O: eq O O
| eq_S {m n}: eq m n -> eq (S m) (S n)
| eq_Sup {p q}: map eq p q -> eq (Sup p) (Sup q)
.

Fixpoint ord_induction {P}
         (onO: P O O)
         (onS: forall (x y: ord), P x y -> P (S x) (S y))
         (onSup: forall (f g: stream ord), map P f g -> P (Sup f) (Sup g))
         (x y: ord) (p: eq x y) {struct p}: P x y.
Proof.
  destruct p.
  - apply onO.
  - apply onS.
    apply (ord_induction _ onO onS onSup).
    auto.
  - apply onSup.
    refine (stream_prod _ _ _ _ m).
    + intros.
      apply (ord_induction _ onO onS onSup).
      destruct H.
      auto.
    + intros.
      destruct H.
      apply H.
Defined.