Feat(kernel): give which part failed conversion in `NotDefEq`
Right now, whenever conversion between two terms fail and a NotDefEq error is raised, the error may print out giant terms even though the error is very localized. When two terms are found to not be defeq, conversion
should give the two subterms that failed to unify in order for them to be added to the NotDefEq
error.