proposition: Fact fot_word_var_eq t : t = fot_word_var (fot_word t) (fot_var t).
proof: Proof. induction t as [ | s v IH ]; simpl in *; auto; f_equal. generalize (IH pos0); clear IH; vec split v with t; vec nil v; clear v; simpl. intros; f_equal; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec 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 fo_logic fo_sat Sig_no_syms)