Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
datatype_iter()
Enum()
InductiveRel()
accessor_lemmas()
accessor_num()
constructor_num()
datatype_call()
datatype_len()
datatype_match_()
datatype_replace()
distinct_lemmas()
inj_lemmas()
multipattern_match()
pattern_match()
recognizer_lemmas()
rel
Enable iteration over constructors of a datatype sort
self (DatatypeSortRef)
Iterator[DatatypeRef]