Skip to content

fix the proof of find_uniq under mathcomp version 1.8

Sergey Bozhko requested to merge RT-PROOFS/rt-proofs:master into master

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.

Merge request reports