proposition: Fact fol_rels_subst σ (A : 𝔽) : fol_rels (A⦃σ⦄) = fol_rels A.
proof: Proof. revert σ. induction A as [ | s r | b A HA B HB | q A HA ]; intros f; simpl; auto. rewrite HA, HB; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms) Undecidability.Shared.ListAutomation