Function match_expr_pattern 

pub fn match_expr_pattern(
    pattern: &ProofExpr,
    target: &ProofExpr,
) -> Option<Substitution>

One-sided match of an expression pattern against a target (see match_term_pattern). Quantified subexpressions match name-strictly (no alpha-renaming — conservative: an alpha-variant simply fails), and a pattern variable never binds a term that mentions a bound variable (capture is rejected, not silently permitted).