pub fn beta_reduce<'a>(
expr: &'a LogicExpr<'a>,
expr_arena: &'a Arena<LogicExpr<'a>>,
term_arena: &'a Arena<Term<'a>>,
) -> &'a LogicExpr<'a>Expand description
Performs beta reduction on lambda applications.
Reduces (λx.body)(arg) to body[x := arg] by substituting
the argument for the bound variable in the body.