The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Roly Perera wrote:
> I get the feeling that what I actually need to do is define my App
> constructor in terms of a function from fmember to terms, but the
> problem seems to be instantiating term with the right type whilst
> keeping the inductive type well-formed (i.e. avoiding 'Non strictly
> positive occurrence of "term"').
>   

I expect this is what you're looking for:
   | App (ls: list type) (c: type): (forall c', fmember _ c' ls -> term 
c') -> term c.

Your original type for [App] doesn't look much like a usual application 
typing rule, in that it omits connections between the types of different 
parts, but I'm assuming that's a conscious simplification that you made.