fact: Fixpoint subst_many (s : term) n (ts : list term) := match s with | var x => nth x (map var (seq 0 n) ++ ts) (var x) | app s t => app (subst_many s n ts) (subst_many t n ts) | lam s => lam (subst_many s (S n) ts) end.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun