fact: Definition ax_ind phi := phi[∅..] → (∀ ∀ phi[$0 .: (fun n => $(2+n))] → phi[$1 .: (fun n => $(2+n))] → phi[$0 ::: $1 .: (fun n => $(2+n))]) → ∀ phi.
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.FOL.Sets.Signatures List