Trees with [in]finite branches

Define four predicates on potentially infinite binary trees :
For each of the preceding predicates, build an example tree, then prove that it satisfies this predicate.
Prove the following theorems (for any tree t) :

Resources

Use the solution of all preceding exercises of this thread.

Caution

Please remind that you've just defined these four predicates, and can't argue that "being infinite" is just the negation of "being finite".
Moreover, the last theorem of the list above can't be proved in the intuitionnistic framework of Coq, since knowing that not every branch of t is finite doesn't help you to build an infinite branch ! You can use Coq's classical module, or just open a section like that :
Section classic.
 Hypothesis class : forall P:Prop, ~~P->P.
...

Solution

Follow this link