Rule set for certified formula synthesis

FODefinable contains compositional certificates that synthesize a single well-formed formula from a Lean predicate across a family of structures. Logical extensions can register their own semantic operations in this rule set. The tactic is defined in CslibFrontier.Tactic.FOOperator.