proposition: Lemma many_beta k (v : Vector.t term k) s : (forall x, Vector.In x v -> proc x) -> many_app (many_lam k s) v == many_subst s 0 v.
proof: Proof. induction v in s |- *; cbn; intros Hv. - reflexivity. - rewrite equiv_many_app_L. 2:{ eapply beta_red. eapply Hv. econstructor. reflexivity. } rewrite subst_many_lam. replace (n + 0) with n by lia. rewrite IHv. reflexivity. intros. eapply Hv. now econstructor. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List