proposition: Lemma equiv_eval_equiv s t o : s == t -> s ⇓ o <-> t ⇓ o.
proof: Proof. intros H. split; now rewrite H. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)