The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

In this particular case, where [LC] is a definitional type class, you can directly write:

Class LC T := 

  lc : T -> Prop .

Inductive term := pair (t u : term) | atom.

Inductive LC_term : LC term :=

  LC_term1 t u : lc t -> lc u -> lc (pair t u).

This is because [LC term] unfolds to the arity [term -> Prop] and 

constructors are typechecked in a context where [LC_term : LC term]

so you have your recursive instance available.

You get your induction principle for free:

About LC_term_ind.

(*

LC_term_ind :

∀ P : term → Prop,

(∀ t u : term, lc t → P t → lc u → P u → P (pair t u))

→ (∀ t : term, LC_term t → P t)

*)

You then just have to add: [Existing Instance LC_term] to register it,

Ah, that certainly makes it a lot cleaner, thanks! Is it possible to do something similar for recursive functions? Say,

Class Permute T :=
  permute : Permutation -> T -> T.

and then use permute in recursive calls?

Edsko