proposition: Lemma v1_to_v2_ex ar (v1 : vec D1 ar) : exists v2, v1 ≈ v2.
proof: Proof. Proof using M2_correct M1_correct. induction v1. - now exists []. - destruct IHv1 as [v2 IH]. destruct (F_total h) as [y H]. now exists (y::v2). Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)