proposition: Lemma F_injective : forall x x' y, F x y -> F x' y -> x = x'.
proof: Proof. Proof using M2_correct M1_correct. intros x x' y. revert y x x'. apply (induction M2 M2_correct (fun y => forall x x', F x y -> F x' y -> x = x')). - intros x x'' H1 H2. now rewrite (F_inv4 x), (F_inv4 x''). - intros y IH x x' H1 H2. destruct (F_inv6 x y H1) as [z ->], (F_inv6 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)