The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

This isn't possible as-is in Coq, it's an instance of what you would call *induction recursion*. It's possible to simulate it with -impredicative-set (see here: http://fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html) but I wouldn't recommend it. Instead it's probably better to have an additional parameter for Term, say of all variables which appear free:

Term : forall A B W, (list nat) -> Type

With according constructors. There's a lot of stuff written on building types of terms with binders where only well-formed terms are well-typed. Sadly, a survey article seems hard to find. I kind of like these slides though:

http://www.chargueraud.org/talks/2006_09_13_talk_inria_binders.pdf

On Tue, Feb 16, 2016 at 12:38 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

// Somehow I wrote answer but it got lost and wasn't send.
 

Thank you, but this isn't good enough. If my idea isn't possible, then I will simply write inductive definition of Term, then Fixpoint on it (smth like term_is_correct) and use it inside type { T | term_is_correct T}. 
But it would be unsatisfying for me. Because I need only correct Term instances (with correct bindings inside of them) and have no use for incorrect ones. :|
 
If such mutual definition - of an inductive type which uses (in definition) a fixpoint defined on it - isn't possible in Coq, I will, of course, accept it and use sigma type.