(*Dummy theory to document dependencies *) fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"