fix the proof of find_uniq under mathcomp version 1.8

The proof got stuck at the goal of

 {in l1, forall x0 : T, x0 != x}

which requires unfolding of prop_in1 to get at the x0 before intros can be effective.

This still compiles with mathcomp version 1.7.