Function apply_subst_to_term 

pub fn apply_subst_to_term(term: &ProofTerm, subst: &Substitution) -> ProofTerm

Apply a substitution to a term.

Replaces all variables in the term according to the substitution mapping. Handles transitive chains: if {x ↦ y, y ↦ z}, then applying to x yields z.

Arguments

• term - The term to transform
• subst - The substitution mapping variables to replacement terms

Returns

A new term with all substitutions applied.

Example

use logicaffeine_proof::{ProofTerm, unify::{Substitution, apply_subst_to_term}};
use std::collections::HashMap;

let mut subst = Substitution::new();
subst.insert("x".into(), ProofTerm::Constant("Socrates".into()));

let term = ProofTerm::Function(
    "Mortal".into(),
    vec![ProofTerm::Variable("x".into())]
);

let result = apply_subst_to_term(&term, &subst);
// result = Mortal(Socrates)