proposition: Lemma F_mul : forall x x' y y', F x y -> F x' y' -> F (x i⊗1 x') (y i⊗2 y').
proof: Proof. Proof using M2_correct M1_correct. apply (induction M1 M1_correct (fun x => forall x' y y', F x y -> F x' y' -> F (x i⊗1 x') (y i⊗2 y'))). - intros x' y y' H1 H2. rewrite (F_inv3 y H1). rewrite (mul_zero M1), (mul_zero M2); try easy. exact F_O. - intros x'' IH x' y y' H1 H2. destruct (F_inv5 x'' y H1) as [y'' ->]. rewrite (mul_rec M1), (mul_rec M2); try easy. apply F_add. exact H2. apply IH. now apply F_inv7. exact H2. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)