proposition: Lemma F_inv5 : forall x y, F (S1 x) y -> exists y', y = S2 y'.
proof: Proof. Proof using M2_correct M1_correct. intros x y. destruct (case_analysis M2 M2_correct y) as [->|[y' ->]]. - now intros H%F_inv1. - intros _. now exists y'. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)