Inductive Tok := varT (n :nat) | appT | lamT | retT.
Notation Pro := (list Tok) (only parsing).
Instance Tok_eq_dec : eq_dec Tok.
repeat intro. hnf. repeat decide equality.
Qed.
Fixpoint compile (s: L.term) : Pro :=
match s with
var x => [varT x]
| app s t => compile s ++ compile t ++ [appT]
| lam s => lamT :: compile s ++ [retT]
end.
Inductive reprP : Pro -> term -> Prop :=
reprPC s : reprP (compile s) (lam s).