proposition: Lemma F_inv4 x : F x O2 -> x = O1.
proof: Proof. Proof using M2_correct M1_correct. destruct (case_analysis M1 M1_correct x) as [->|[x' ->]]. - easy. - now intros H%F_inv1. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)