proposition: Lemma P1_to_P2 ar (P1 : vec D1 ar -> Prop) : { P2 | P1 ≈ P2 }.
proof: Proof. Proof using M2_correct M1_correct. exists (fun v => forall v', Forall2 F v' v -> P1 v'). intros v1 v2 H1. split. - intros H2 v' H3. induction v' as [|? ? ? IHv']. + revert H2. pattern v1. now apply Vector.case0. + revert H1 H2. apply (Vector.caseS' v1). intros. assert (h = h0) as ->. { apply eq1_sem. easy. eapply F_eq. apply H3. apply H1. now apply eq2_sem. } assert (v' = t) as ->. { eapply IHv'. apply H1. reflexivity. apply H3. } exact H2. - firstorder. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)