Propositional equality is a partial order with respect to itself

[MatthewDaggitt]

No description provided.

[Taneb]

Isn't this true of any equivalence relation? Could we make this more general?

[MatthewDaggitt]

You're right, we could add this to Relation.Binary.Properties.Setoid. Will do.

[jamesmckinna]

Revisiting this briefly in the context of #1437 / #1836: does this mean that we could unify once and for all the disparate uses of ≤-Reasoning and ≡-Reasoning and their associated combinators and syntax declarations (it always seems strange to write begin-equality for a proof involving ≤-Reasoning, and that need to be distinct from begin for one involving ≡-Reasoning... etc.)

[JacquesCarette]

That sure would be nice!