https://stackoverflow.com/questions/76254112/non-trivial-fixpoint-on-nested-recursive-types

encode.v

From Coq Require Import List.
Import ListNotations.

Inductive bintree : Type :=
  | Leaf : bintree
  | Node : bintree -> nat -> bintree -> bintree.

Inductive tree :=
  | TNode : nat -> list tree -> tree.

Module Ex1.

Definition append (t t' : bintree) : bintree :=
  match t with
  | Leaf => Leaf (* useless *)
  | Node l n _ => Node l n t'
  end.

Fixpoint encode (t : tree) : bintree :=
  let fix encode_list ts' :=
    match ts' with
    | [] => Leaf
    | t' :: ts' => append (encode t') (encode_list ts')
    end in
  match t with
  | TNode n ts => Node (encode_list ts) n Leaf
  end.

End Ex1.

Module Ex2.

Fixpoint append_encode (t : tree) (w : bintree) : bintree :=
  let fix encode_list ts' :=
    match ts' with
    | [] => Leaf
    | t' :: ts' => append_encode t' (encode_list ts')
    end in
  match t with
  | TNode n ts => Node (encode_list ts) n w
  end.

Definition encode (t : tree) : bintree := append_encode t Leaf.

End Ex2.