A polymorphic functional

Consider the following definitions :
Unset Implicit Arguments.

Definition compose (A:Set) (g f:A -> A) (x:A) := g (f x).

Definition thrice (A:Set) (f:A -> A) := compose A f (compose A f f).
Build an expression, the normal form of which is 27, using only two occurrences of thrice, one occurrence of S, one occurrence of (0) and two jokers (symbol '_' ).
Same question, without using jokers.

Solution

Look at this file


Going home
Pierre Castéran