proposition: Fact subst_Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) sigma: subst_form sigma (Fr phi) = Fr (subst_form sigma phi).
proof: Proof. revert sigma. induction phi; cbn. - reflexivity. - now unfold dn. - destruct b0; cbn; unfold dn, Q; congruence. - destruct q; cbn; intros sigma; unfold dn, Q; congruence. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)