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.

Hi Björn, indeed, the old proof doesn't work with mathcomp 1.8. But the good news is that this is the only proof that breaks. So, (with this fix) I was able to compile the whole project with Coq 8.9.0 and mathcomp 1.8.

Great, thanks for reviewing and testing the fix. I'll go ahead and merge then.

closed

reopened

merged