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