Due to a bug, eauto neglected the cost of the extern hint lia (and applied it first). However, if lia is applied last, then some non-useful low-cost hints introduce evars beforehand, which breaks the proof. Changing eauto to auto at the specific position would avoid the evar issue.