proposition: Lemma iso_vec_eq2 ar (v1 : vec D1 ar) v2 v2' : v1 ≈ v2 -> v1 ≈ v2' -> v2 = v2'.
proof: Proof. Proof using M2_correct M1_correct. intros H1 H2. induction v2 as [|? ? ? IHv2]. - pattern v2'. now apply Vector.case0. - revert H2. apply (Vector.caseS' v2'). revert H1. apply (Vector.caseS' v1). intros. f_equal. eapply F_functional. apply H1. apply H2. eapply IHv2. apply H1. apply H2. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)