Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to store the children.Inductive LTree : Set := Node : list LTree -> LTree.The naive way of defining a recursive function over these trees by recursing over trees and lists of trees does not work. Here's an example with the size function that computes the number of nodes.Fixpoint size (t : LTree) : nat := match t with Node l => 1 + (size_l l) endwith size_l (l : list LTree) : nat := match l with    | nil => 0    | cons h r => size h + size_l r  end.This definition is ill-formed (error message excerpted):Error:Recursive definition of size_l is ill-formed.Recursive call to size has principal argument equal toh instead of r.Why is the definition ill-formed, even though r is clearly a subterm of l? Is there a way to define recursive functions on such a data structure?If you aren't fluent in Coq syntax: LTree is an inductive type corresponding to the following grammar.$$\begin{align}   \mathtt{LTree} ::= & \\   \vert & \mathtt{list}(\mathtt{LTree}) \\ \end{align}$$We attempt to define the size function by induction over trees and lists. In OCaml, that would be:type t = Node of t listlet rec size = function Node l -> 1 + size_l land size_l = function [] -> 0                    | h::r -> size h + size_l r
Recursive definitions over an inductive type with nested components
logic;coq;type theory;recursion;proof assistants