proposition: Lemma eval_ext rho1 rho2 t : (forall n, get_indi rho1 n = get_indi rho2 n) -> (forall n ar v, get_func rho1 n ar v = get_func rho2 n ar v) -> eval rho1 t = eval rho2 t.
proof: Proof. intros H1 H2. induction t. - apply H1. - cbn. enough (map (eval rho1) v = map (eval rho2) v) as -> by apply H2. now apply map_ext_forall. - cbn. f_equal. now apply map_ext_forall. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector