Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Record()
axiom()
cond()
define()
lemma()
kbo()
HornClause
Order
Rule
alpha_eq()
apply()
decl_index()
decls()
expr_to_lean()
generate()
horn_of_theorem()
is_subterm()
is_value()
lemma_db()
lpo()
occurs()
open_binder()
pmatch()
pmatch_rec()
prompt()
quant_kind_eq()
rewrite()
rewrite1()
rewrite_star()
rule_of_theorem()
simp()
simp2()
sorts()
subterms()
unify_db()
Knuth Bendix Ordering, naive implementation. All weights are 1. Source: Term Rewriting and All That section 5.4.4