proposition: Lemma F_eq : forall x x' y y', F x y -> F x' y' -> (x =1= x' <-> y =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' -> (x =1= x' <-> y =2= y'))). - intros x' y y' H1 H2. split. + intros H3%eq1_sem. rewrite <- H3 in H2. rewrite (F_inv3 y H1). rewrite (F_inv3 y' H2). now apply eq2_sem. easy. + intros H3%eq2_sem. rewrite <- H3 in H2. rewrite (F_inv3 y H1) in H2. rewrite (F_inv4 x' H2). now apply eq1_sem. easy. - intros x IH x' y y' H1 H2. split. + intros H3%eq1_sem. rewrite <- H3 in H2. destruct (F_inv5 x y H1) as [z ->]. destruct (F_inv5 x y' H2) as [z' ->]. enough (z =2= z') as ->%eq2_sem by (try easy; now apply eq2_sem). apply (IH x). now apply F_inv7. now apply F_inv7. now apply eq1_sem. easy. + intros H3%eq2_sem. rewrite <- H3 in H2. destruct (F_inv5 x y H1) as [z ->]. destruct (F_inv6 x' z H2) as [x'' ->]. enough (x =1= x'') as ->%eq1_sem by (try easy; now apply eq1_sem). apply (IH x'' z z). now apply F_inv7. now apply F_inv7. now apply eq2_sem. easy. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)