The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> But what if I want to write "supremum S == supremum T"? (to add more 
> complexity, the first and the second supremum may be taken on different 
> sets.)

You coudl write for example as

   exists x, supremum S x /\ supremum T x

and presumably you would want to prove

  Lemma suprema_unique (A : Poset) (S : A -> Prop) (x y : A) :
supremum S x -> supremum S y -> x = y.

But if you have a lot of suprema and you work with complete posets,
then it might be better to formalize complete posets with an actual
operation "sup", so you could just write "sup S = sup T".

With kind regards,

Andrej