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