fact: Fixpoint subst (sigma: nat -> term) (s: term) : term := match s with | var n => sigma n | app s t => app (subst sigma s) (subst sigma t) | lam s => lam (subst (scons (var 0) (funcomp (ren S) sigma)) s) end.
imports: Relation_Operators