proposition: Lemma beta_red s t t' : lambda t -> t' == subst s 0 t -> (lam s) t == t'.
proof: Proof. intros [u ->] ->. repeat econstructor. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List