fact: Definition apply_encs_to (s : term) k := ((Vector.fold_left (fun s n => ext L.app s (ext (@enc X _) (var n))) s (many_vars k))).
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)