Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
kbo()
Order
RewriteRule
RewriteRuleException
Rule
apply()
decl_index()
def_eq()
horn_of_theorem()
lpo()
rewrite()
rewrite1()
rewrite1_rule()
rewrite_star()
rule_of_theorem()
simp1()
simp2()
unfold()
Knuth Bendix Ordering, naive implementation. All weights are 1. Source: Term Rewriting and All That section 5.4.4
vs (list[ExprRef])
t1 (ExprRef)
t2 (ExprRef)