Writing a first-order induction schema as Mathlib ModelTheory sentences (relabel + subst + iAlls)

For φ : L.Formula (Fin (k+1)), where free var 0 is the induction variable and the rest are parameters, build the instance with these pieces. φx := φ.relabel (Fin.cons (Sum.inr 0) Sum.inl) : Formula (Fin k ⊕ Fin 1). φ0 := φ.subst (Fin.cons 0 fun i => var i). φs := φ.subst (Fin.cons (var (Sum.inr 0) + 1) fun i => var (Sum.inl i)). Quantify the induction variable with Formula.iAlls (Fin 1) and close the parameters with Formula.iAlls (Fin k) (body.relabel Sum.inr). Then simp only [Formula.realize_iAlls, Formula.realize_relabel, Formula.realize_imp, Formula.realize_inf] gives the semantic schema. You also need two helper facts, each proved by funext + Fin.cases: Sum.elim v i ∘ g = Fin.cons (i 0) v, and the substituted valuation equals Fin.cons (i 0 + 1) v. Gotchas: φ.subst elaborates as BoundedFormula.subst, so state your own Formula.Realize (φ.subst tf) v ↔ ... (proof: BoundedFormula.realize_subst). Write Formula.iAlls (Fin 1) (a ⟹ b) rather than (a ⟹ b).iAlls, because ⟹ returns a BoundedFormula and the field lookup fails.