pub fn normalize(ctx: &Context, term: &Term) -> Term
Normalize a term to its normal form.
Repeatedly applies reduction rules until no more reductions are possible. This is a full normalization that reduces under binders.