'From' Keyword.Namespace ' ' Text 'Coq' Name ' ' Text 'Require' Keyword.Namespace ' ' Text 'Import' Keyword.Namespace ' ' Text 'Arith' Name '.' Operator '\n' Text 'Require' Keyword.Namespace ' ' Text 'Import' Keyword.Namespace ' ' Text 'Equations.Prop.Equations' Name '.' Operator '\n' Text 'Set' Keyword.Namespace ' ' Text 'Implicit' Keyword.Namespace ' ' Text 'Arguments' Keyword.Namespace '.' Operator '\n' Text 'Set' Keyword.Namespace ' ' Text 'Primitive' Name ' ' Text 'Projections' Keyword.Namespace '.' Operator '\n' Text 'Unset' Keyword.Namespace ' ' Text 'Printing' Keyword.Namespace ' ' Text 'All' Keyword.Namespace '.' Operator '\n' Text 'Scheme' Keyword.Namespace ' ' Text 'tree_forest_rec' Name ' ' Text ':=' Operator ' ' Text 'Induction' Name ' ' Text 'for' Keyword ' ' Text 'tree' Name ' ' Text 'Sort' Name ' ' Text 'Set' Keyword.Type '\n ' Text 'with' Keyword ' ' Text 'forest_tree_rec' Name ' ' Text ':=' Operator ' ' Text 'Induction' Name ' ' Text 'for' Keyword ' ' Text 'forest' Name ' ' Text 'Sort' Name ' ' Text 'Set' Keyword.Type '.' Operator '\n' Text 'Fail' Keyword.Namespace ' ' Text 'Definition' Keyword.Namespace ' ' Text 'x' Name ' ' Text ':' Operator ' ' Text 'unit' Name ' ' Text ':=' Operator ' ' Text '3' Literal.Number.Integer '.' Operator '\n' Text 'admit' Keyword.Pseudo '.' Operator '\n' Text 'Equations?' Keyword.Namespace ' ' Text 'neg' Name ' ' Text '(' Operator 'b' Name ' ' Text ':' Operator ' ' Text 'bool' Name ')' Operator ' ' Text ':' Operator ' ' Text 'bool' Name ' ' Text ':=' Operator '\n' Text 'neg' Name ' ' Text 'true' Name.Builtin.Pseudo ' ' Text ':=' Operator ' ' Text 'false' Name.Builtin.Pseudo ';' Operator '\n' Text 'neg' Name ' ' Text 'false' Name.Builtin.Pseudo ' ' Text ':=' Operator ' ' Text 'true' Name.Builtin.Pseudo '.' Operator '\n' Text