proposition: Lemma env_contains_PA2_scons_f {rho rho' xO xS xA xEq ar} (f : vec D ar -> D) : env_contains_PA2 rho rho' xO xS xA xEq -> match ar with | 0 => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ (S xO) xS xA xEq | 1 => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO (S xS) xA xEq | 2 => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO xS (S xA) xEq | _ => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO xS xA xEq end.
proof: Proof. intros E. unfold econs, econs_func, econs_ar. destruct ar as [|[|[]]]; split; try apply E; split; try apply E; destruct E as [_ [E2 _]]; intros [|[|[]]] [|[|[]]]; rewrite ?insert_0_S, ?insert_S_S. all: cbn; destruct Nat.eq_dec; try easy. all: etransitivity; [apply E2|try reflexivity]. all: apply insert_ext'; intros ?; now rewrite insert_S_S. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec