The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

In my opinion, your 'leaves' function exists in a world just slightly 
beyond pure Coq, but not beyond HOL,
for instance.

let us consider the following function of type nat -> cotree -> nat

Fixpoint f (n:nat)(t:cotree) : nat :=
 match n with
   0 => 0
 | S p =>
   match t with
     coleaf => 1
   | cobranch t1 t2 => f p t1 + f p t2
   end
 end.


This is a plain structural recursive function in n.  Given a cotree t, 
you can consider the sequence
 fun x => f x t
I believe it must be fairly easy to show that this sequence is always 
increasing.

Using the excluded-middle axiom, you can reason  on whether this 
sequence is bound or whether it goes to infinity, using Hilbert's choice 
operator you can use this to define a function of type cotree -> option nat,
where None would be used to represent infinity.  The axiom for excluded 
middle and Hilbert's choice operator are provided in HOL's theory.

You could probably also model the 'leaves' function inside Coq augmented 
with ClassicalEpsilon.

Yves