pub fn unify<'a, T>( s: &'a Term<T>, t: &'a Term<T>, ) -> Option<HashMap<&'a Term<T>, &'a Term<T>>>where T: Eq + Hash,