proposition: Fact nat_induction phi : forall rho, sat interp_nat rho (ax_induction phi).
proof: Proof. intros rho H0 IH d. induction d; cbn in *. rewrite <-sat_single in H0. apply H0. apply IH in IHd. rewrite sat_comp in IHd. revert IHd. apply sat_ext. intros []; reflexivity. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector