Function unify_exprs 

pub fn unify_exprs(e1: &ProofExpr, e2: &ProofExpr) -> ProofResult<Substitution>

Unify two expressions, returning the Most General Unifier.

Expression unification extends term unification with support for logical connectives, quantifiers, and alpha-equivalence for bound variables.

Alpha-Equivalence

Bound variable names are considered arbitrary:

• ∀x P(x) unifies with ∀y P(y)
• ∃e Run(e) unifies with ∃x Run(x)

This is achieved by substituting fresh constants for bound variables before comparing bodies.

Beta-Reduction

Both expressions are beta-reduced before comparison, so (λx. P(x))(a) will unify with P(a).

Arguments

• e1 - The first expression
• e2 - The second expression

Returns

• Ok(subst) - A substitution unifying the expressions
• Err(ExprUnificationFailed) - If expressions cannot be unified

See Also

• unify_terms - Underlying term unification
• beta_reduce - Normalization applied before unification
• unify_pattern - Higher-order pattern unification for holes