proposition: Lemma eq_sem x y : x i== y <-> x = y.
proof: Proof. Proof using M_correct. split. - revert x y. apply (induction (fun x => forall y, x i== y -> x = y)). + intros y H. destruct (case_analysis y) as [->|[y' ->]]. * reflexivity. * now apply zero_succ' in H. + intros x IH y H. destruct (case_analysis y) as [->|[y' ->]]. * now apply eq_symm, zero_succ' in H. * rewrite (IH y'). reflexivity. now apply succ_inj'. - intros ->. apply eq_reflexive. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec