Information Flow Inference for Free, step 1

(* based on Pottier and Conchon, Information
    Flow Inference for Free *)

Require Import Autosubst.

(* as in the original paper, for now we leave
     the set of labels entirely abstract *)

Inductive term {label : Set}  : Type :=
| Const (k : nat)
| Var (x : var)
| Abs (s : {bind term})
| App (s t : term)
| Let (s : term) (t : {bind term})
| Label (s : term) (l : label).

Instance Ids_term (label : Set) : Ids (term (label := label)). derive. Defined.
Instance Rename_term (label : Set) : Rename (term (label := label)). derive. Defined.
Instance Subst_type (label : Set) : Subst (term (label := label)). derive. Defined.

(* does not derive: produces "Error: Tactic failure" *)
Instance SubstLemmas_term (label : Set) : SubstLemmas (term (label := label)). derive.