whd-beta reduction before instantiation
widened the intersection of substitutions for same evar to allow arbitrary terms in the substitution, as long as they are equal in both substitution
forgot to commit the mli file