The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Damien Andrew Tamburri wrote:
>     I am having difficulty in including the context for rules in 
> Natural Deduction, within a structure representing Natural Deduction 
> Trees themselves (see attached file).. I keep getting the "The term 
> "In a X" has type "Prop" which is not a (co-)inductive type." error 
> for the last three constructors of type NDTree.. can anyone explain me 
> if and how I can use the construct "if..then..else" in this way? what 
> other context alternatives are there?

Like the error message suggests, [if..then..else] is for analyzing
values of inductive types that have two constructors (e.g., [bool]).  It
doesn't make sense that you'd be able to use the same construct to
analyze a [Prop], since [if..then..else] is very computational, and
truth of [Prop]s is undecidable in general.

Try to find a way to express what you want using implication instead.
You don't have many other options available within an inductive type
definition, because of the positivity criterion.