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