proposition: Lemma induction (P : M_domain M -> Prop) : P izero -> (forall x, P x -> P (iσ x)) -> forall x, P x.
proof: Proof. Proof using M_correct. pose (P' := fun v : vec _ 1 => P (Vector.hd v)). change (P' ([izero]) -> (forall x, P' ([x]) -> P' ([iσ x])) -> forall x, P' ([x])). apply (M_correct ax_ind ltac:(easy) (empty_PA2_env _)). 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