title: Consistency of Inductive propositions
body: <p>In coq, defining an inductive proposition seems analogous to adding new inference rules/axioms to a logic. What constraints in defining an inductive proposition guarantees that coq remains consistent?</p>