Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Another thing about the script that got me thinking was:

> Lemma trivIsetEn (T : finType) (P : {set {set T}}) :
>   ~~ trivIset P =
>   [exists A in P, [exists B in P, (A != B) && (A :&: B != set0)]].

Which is basically a restatement of trivIsetP. In fact, if you at the
code, we have basically proved nothing new.

I'm talking very speculatively given that I don't know what the final
theorem is, but maybe I'd try to avoid introducing this lemma and the
computation of the sets A B altogether and try to derive the final proof
directly from trivIsetP.

Best regards,
Emilio