• Here should be explained some of the mysteries behind Coq guard condition for fixpoints
• All arguments of constructors are NOT admissible sub terms