proposition: Fact fol_def_subst2 R t1 t2 : fol_definable ls lr M (fun φ => R (φ 0) (φ 1)) -> fot_definable ls M t1 -> fot_definable ls M t2 -> fol_definable ls lr M (fun φ => R (t1 φ) (t2 φ)).
proof: Proof. intros H1 H2 H3. set (f n := match n with | 0 => t1 | 1 => t2 | _ => fun φ => φ 0 end). change (fol_definable ls lr M (fun φ => R (f 0 φ) (f 1 φ))). apply fol_def_subst with (2 := H1) (f := f). intros [ | [ | n ] ]; simpl; fol def. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)