proposition: Lemma many_subst_apply_encs_to s n (u : Vector.t term n) : closed s -> (forall x, Vector.In x u -> closed x) -> many_subst (apply_encs_to s n) 0 u = ((Vector.fold_left (fun s n => ext L.app s (ext (@enc X _) n)) s u)).
proof: Proof. induction u in s |- *; intros Hs Hu; cbn -[many_vars]. - reflexivity. - unfold apply_encs_to. rewrite many_vars_S. cbn. unfold apply_encs_to in IHu. rewrite <- IHu. fold (apply_encs_to (ext L.app s (ext (@enc X _) n)) n). rewrite subst_apply_encs_to. 2:lia. unfold apply_encs_to. repeat f_equal. cbn. repeat (rewrite subst_closed; [| now Lproc]). now rewrite Nat.eqb_refl. assert (closed h) as Hh. eapply Hu. econstructor. Lproc. intros. eapply Hu. now econstructor. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)