Function deepen_stack_all 

pub fn deepen_stack_all<R: Send>(
    terms: &[&Term],
    f: impl FnOnce() -> R + Send,
) -> Option<R>

deepen_stack for an entry point that takes more than one term — is_subtype and def_eq compare two, and the stack has to hold the DEEPER of them.