Function transfer 

pub fn transfer(
    reduction: &Reduction,
    source_steps: &[ProofStep],
    ranks: &[u64],
    target_formula: &[Vec<Lit>],
) -> Option<RankedRefutation>

The transfer functor. Carry a refutation/measure of F' to one of F along ρ, preserving the level structure (ranks). Re-checks the transferred proof against F (fail-closed): returns the transferred ranked refutation iff it genuinely refutes the target. Functorial — transfer along the identity reduction is the identity, and along a composite is the composite.