The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

// 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.