proposition: Lemma form_ind_subst : forall P : form -> Prop, P falsity -> (forall P0 (t : vec term (ar_preds P0)), P (atom P0 t)) -> (forall (b0 : binop) (f1 : form), P f1 -> forall f2 : form, P f2 -> P (bin b0 f1 f2)) -> (forall (q : quantop) (f2 : form), (forall sigma, P (subst_form sigma f2)) -> P (quant q f2)) -> forall (f4 : form), P f4.
proof: Proof. apply (form_ind_subst' (ff := falsity_on)). Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat Nat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts