pub fn is_convertible(left: &Node, right: &Node, env: &mut Env) -> bool
Decide whether two terms are definitionally equal under the current environment using beta-normalization and explicit equality assignments.