**Abstract** : Proof systems like Coq feature inductive datatypes, where datatype constructor- s are free in the sense that two terms built from constructors only are semantically equal if and only if they are syntactically identical. Although free constructors are an essential ingredient of modern formalized mathematics- , no automated first-order prover has been specialized with built-in rules for dealing with free constructors, until now. We propose a sequent system for a logic where terms can be built only from variables and free constructors- . Thus the logic will be kept simple, as equality in the logic will be syntactical equality. We show how partial functions can be introduced into the logic, in the form of predicates obeying some functionality constrain- ts. We prove that the resulting system is sound and complete with respect to a natural first-order semantics of datatypes, and enjoys cut elimination. We then develop a tableau calculus to find proofs in this sequent system. This involves solving an extended form of unification, which unfortunately is undecidable: we show that it indeed includes second-order predicate unification as a subproblem. Nonetheless, we describe a non-terminating procedure to solve such unification problems, and give a few hints so as to improve its efficiency in practice. Finally, we extend the system to include first-order structural induction principles on datatype values. This does not pose any difficulty, apart from the expected problem of induction loading-namely, that we may need to generalize a proposition before we can prove it by induction.