proposition: Lemma F_total : forall x, exists y, F x y.
proof: Proof. Proof using M2_correct M1_correct. apply (induction M1 M1_correct). - exists O2. exact F_O. - intros x [y IH]. exists (S2 y). now apply F_S. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)