proposition: Lemma F_inv7 x y : F (S1 x) (S2 y) -> F x y.
proof: Proof. Proof using M2_correct M1_correct. intros H. inversion H. + exfalso. now apply (zero_succ M1 M1_correct x). + apply (succ_inj M1 M1_correct) in H0 as ->. apply (succ_inj M2 M2_correct) in H1 as ->. exact H2. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)