fact: Fixpoint substList (s:term) (x:nat) (A: list term): term := match s with | var n => if Dec (x>n) then var n else nth (n-x) A (var n) | app s t => app (substList s x A) (substList t x A) | lam s => lam (substList s (S x) A) end.