In analogy to the equivalence lemmas for recursive function definitions,
the introduction rules of a (co)inductive predicate are output as proof
obligations in realization mode if syntax has been declared for the
predicate.