proposition: Lemma form_ind_subst' {ff : falsity_flag} : forall P : form -> Prop, (match ff return ((form Σ_funcs Σ_preds ops ff) -> Prop) -> Prop with | falsity_off => fun _ => True | falsity_on => fun P' => P' falsity end) P -> (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. intros P H1 H2 H3 H4 phi. induction phi using (@size_ind _ size). destruct phi; cbn in *. - easy. - apply H2. - apply H3; apply H; lia. - apply H4. intros sigma. apply H. rewrite subst_size. econstructor. 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