Confused about nested inductive coinductive types

Given the following definition of ordinals how would you define a nice induction principle over them?

CoInductive stream A := {
  head: A ;
  tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).

I couldn’t figure out how to use Fixpoint through coinductive types either, but if you replace stream A with nat -> A it’s possible to define

Fixpoint ord_ind (P : ord -> Prop)
    (HO : P O)
    (HS : forall n, P n -> P (S n))
    (HSup : forall f, (forall i, P (f i)) -> P (Sup f))
  : forall n, P n.

Ah well that was what I was planning on avoiding.

And I don’t think there is way to define an isomorphism between

Inductive ord := O | S (n: ord) | Lim (p: nat -> ord).

And the other representation without extensionality which I was maybe thinking of assuming but it’d be nice not to have to use

Full context for an induction principle which doesn’t quite go through.

See also How is coinduction the dual of induction? – Blog – Joachim Breitner's Homepage