Function match_term_pattern 

pub fn match_term_pattern(
    pattern: &ProofTerm,
    target: &ProofTerm,
) -> Option<Substitution>

One-sided match of a term pattern against a target: pattern Variables bind target subterms; the target is inspected, never bound. Repeated pattern variables must bind the same subterm. This is the arbiter behind discrimination-tree retrieval (crate::discrimination) — the tree over-approximates, this decides.