proposition: Lemma equiv_R (s t t' : term): t == t' -> s t == s t'.
proof: Proof. now intros ->. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)