proposition: Lemma F_functional : forall x y y', F x y -> F x y' -> y = y'.
proof: Proof. Proof using M2_correct M1_correct. apply (induction M1 M1_correct (fun x => forall y y', F x y -> F x y' -> y = y')). - intros y y' H1 H2. now rewrite (F_inv3 y), (F_inv3 y'). - intros x IH y y' H1 H2. destruct (F_inv5 x y H1) as [z ->], (F_inv5 x y' H2) as [z' ->]. apply F_inv7 in H1; apply F_inv7 in H2. now rewrite (IH z z'). Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)